diff options
Diffstat (limited to 'contrib/subtac/test/Mutind.v')
| -rw-r--r-- | contrib/subtac/test/Mutind.v | 20 |
1 files changed, 0 insertions, 20 deletions
diff --git a/contrib/subtac/test/Mutind.v b/contrib/subtac/test/Mutind.v deleted file mode 100644 index ac49ca96..00000000 --- a/contrib/subtac/test/Mutind.v +++ /dev/null @@ -1,20 +0,0 @@ -Require Import List. - -Program Fixpoint f a : { x : nat | x > 0 } := - match a with - | 0 => 1 - | S a' => g a a' - end -with g a b : { x : nat | x > 0 } := - match b with - | 0 => 1 - | S b' => f b' - end. - -Check f. -Check g. - - - - - |