diff options
| author |  Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2014-06-03 18:07:18 +0200 |
|---|---|---|
| committer | Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2014-06-04 14:11:33 +0200 |
| commit | 848f2c41e605287c99e84c2f8ea1747c8a34e201 (patch) | |
| tree | 5454e67be508c8dea44db6069455cdcf41dd5ead /test-suite/output | |
| parent | 7d7784230d91f67bdc5a3bf06caab296c64034a8 (diff) | |
cbn understand ! Arguments directive
Of course, this is an under approximation of the expected behavior : unfolding
a constant iff a leaf of its underlying split-tree is reached.
Diffstat (limited to 'test-suite/output')
| -rw-r--r-- | test-suite/output/Arguments.out | 4 | ||||
| -rw-r--r-- | test-suite/output/Arguments.v | 2 |
2 files changed, 6 insertions, 0 deletions
diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out index 5a3578f7d..e0e8211d5 100644 --- a/test-suite/output/Arguments.out +++ b/test-suite/output/Arguments.out @@ -96,6 +96,10 @@ The reduction tactics unfold f when the 5th, 6th and 7th arguments evaluate to a constructor f is transparent Expands to: Constant Top.f + = forall v : unit, f 0 0 5 v 3 = 2 + : Prop + = 2 = 2 + : Prop f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat f is monomorphic diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v index 573cfdab2..4d4ab54f1 100644 --- a/test-suite/output/Arguments.v +++ b/test-suite/output/Arguments.v @@ -36,6 +36,8 @@ End S2. About f. End S1. About f. +Eval cbn in forall v, f 0 0 5 v 3 = 2. +Eval cbn in f 0 0 5 tt 3 = 2. Arguments f : clear implicits and scopes. About f. Record r := { pi :> nat -> bool -> unit }. |