diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /test-suite/success/implicit.v | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'test-suite/success/implicit.v')
-rw-r--r-- | test-suite/success/implicit.v | 44 |
1 files changed, 42 insertions, 2 deletions
diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v index 9034d6a6..59e1a935 100644 --- a/test-suite/success/implicit.v +++ b/test-suite/success/implicit.v @@ -1,3 +1,5 @@ +(* Testing the behavior of implicit arguments *) + (* Implicit on section variables *) Set Implicit Arguments. @@ -12,15 +14,53 @@ Infix "#" := op (at level 70). Check (forall x : A, x # x). (* Example submitted by Christine *) -Record stack : Type := + +Record stack : Type := {type : Set; elt : type; empty : type -> bool; proof : empty elt = true}. Check (forall (type : Set) (elt : type) (empty : type -> bool), empty elt = true -> stack). +(* Nested sections and manual/automatic implicit arguments *) + +Variable op' : forall A : Set, A -> A -> Set. +Variable op'' : forall A : Set, A -> A -> Set. + +Section B. + +Definition eq1 := fun (A:Type) (x y:A) => x=y. +Definition eq2 := fun (A:Type) (x y:A) => x=y. +Definition eq3 := fun (A:Type) (x y:A) => x=y. + +Implicit Arguments op' []. +Global Implicit Arguments op'' []. + +Implicit Arguments eq2 []. +Global Implicit Arguments eq3 []. + +Check (op 0 0). +Check (op' nat 0 0). +Check (op'' nat 0 0). +Check (eq1 0 0). +Check (eq2 nat 0 0). +Check (eq3 nat 0 0). + +End B. + +Check (op 0 0). +Check (op' 0 0). +Check (op'' nat 0 0). +Check (eq1 0 0). +Check (eq2 0 0). +Check (eq3 nat 0 0). + End Spec. +Check (eq1 0 0). +Check (eq2 0 0). +Check (eq3 nat 0 0). + (* Example submitted by Frédéric (interesting in v8 syntax) *) Parameter f : nat -> nat * nat. @@ -42,7 +82,7 @@ Inductive P n : nat -> Prop := c : P n n. Require Import List. Fixpoint plus n m {struct n} := - match n with + match n with | 0 => m | S p => S (plus p m) end. |