diff options
Diffstat (limited to 'test-suite/output/Implicit.out8')
| -rw-r--r-- | test-suite/output/Implicit.out8 | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/test-suite/output/Implicit.out8 b/test-suite/output/Implicit.out8 deleted file mode 100644 index 38c5b827f..000000000 --- a/test-suite/output/Implicit.out8 +++ /dev/null @@ -1,10 +0,0 @@ -compose (C:=nat) S - : (nat -> nat) -> nat -> nat -ex_intro (P:=fun _ : nat => True) (x:=0) I - : ex (fun _ : nat => True) -d2 = fun x : nat => d1 (y:=x) - : forall x x0 : nat, x0 = x -> x0 = x - - -Arguments x, x0 are implicit -Argument scopes are [nat_scope nat_scope _] |