summaryrefslogtreecommitdiff
path: root/test-suite/output/inference.out
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/output/inference.out')
-rw-r--r--test-suite/output/inference.out10
1 files changed, 10 insertions, 0 deletions
diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out
new file mode 100644
index 00000000..4f8de1dc
--- /dev/null
+++ b/test-suite/output/inference.out
@@ -0,0 +1,10 @@
+P =
+fun e : option L => match e with
+ | Some cl => Some cl
+ | None => None
+ end
+ : option L -> option L
+fun n : nat => let x := A n in ?12 ?15:T n
+ : forall n : nat, T n
+fun n : nat => ?20 ?23:T n
+ : forall n : nat, T n