blob: 08078012a978a776a01e1dd2319b4627f20a0ed1 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
(* Kernel test (head term is a constant) *)
Check (fun a : S = S => a : S = fun x => S x).
(* Kernel test (head term is a variable) *)
Check (fun (f:nat->nat) (a : f = f) => a : f = fun x => f x).
(* Test type inference (head term is syntactically rigid) *)
Check (fun (a : list = list) => a : list = fun A => _ A).
(* Test type inference (head term is a variable) *)
(* This one is still to be done...
Check (fun (f:nat->nat) (a : f = f) => a : f = fun x => _ x).
*)
(* Test tactic unification *)
Goal (forall f:nat->nat, (fun x => f x) = (fun x => f x)) -> S = S.
intro H; apply H.
Qed.
|
