summaryrefslogtreecommitdiff
path: root/test-suite/output/inference.out
blob: 4f8de1dcb5950ce8b54c5ef4d346ee42c87575e9 (plain)
1
2
3
4
5
6
7
8
9
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