Mapcard « custom « test « extraction « contrib - debian-coq - Debian packaging for Coq

summary refs log tree commit diff

path: root/contrib/extraction/test/custom/Mapcard

blob: 5932cf7b4b9f087412bfc902dde8d8b27d41f387 (plain)

Require Import Plus.
Extraction NoInline plus_is_one.
Require Import BinNat.
Extraction NoInline Ndouble Ndouble_plus_one.