diff options
Diffstat (limited to 'mathcomp/ssrtest/binders_of.v')
| -rw-r--r-- | mathcomp/ssrtest/binders_of.v | 14 |
1 files changed, 0 insertions, 14 deletions
diff --git a/mathcomp/ssrtest/binders_of.v b/mathcomp/ssrtest/binders_of.v deleted file mode 100644 index 2a88502..0000000 --- a/mathcomp/ssrtest/binders_of.v +++ /dev/null @@ -1,14 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) - -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import seq. - -Lemma test1 : True. -have f of seq nat & nat : nat. - exact 3. -have g of nat := 3. -have h of nat : nat := 3. -have _ : f [::] 3 = g 3 + h 4. -Admitted. |