diff options
| author | Pierre Boutillier | 2014-06-03 18:07:18 +0200 |
|---|---|---|
| committer | Pierre Boutillier | 2014-06-04 14:11:33 +0200 |
| commit | 848f2c41e605287c99e84c2f8ea1747c8a34e201 (patch) | |
| tree | 5454e67be508c8dea44db6069455cdcf41dd5ead /test-suite/output/Arguments.out | |
| 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/Arguments.out')
| -rw-r--r-- | test-suite/output/Arguments.out | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out index 5a3578f7d6..e0e8211d58 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 |