blob: 219d532ac62054b834c9d33c405fa105462681db (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
|
(* Testing recursive notations with binders seen as terms *)
Inductive ftele : Type :=
| fb {T:Type} : T -> ftele
| fr {T} : (T -> ftele) -> ftele.
Fixpoint args ftele : Type :=
match ftele with
| fb _ => unit
| fr f => sigT (fun t => args (f t))
end.
Definition fpack := sigT args.
Definition pack fp fa : fpack := existT _ fp fa.
Notation "'tele' x .. z := b" :=
(
(fun x => ..
(fun z =>
pack
(fr (fun x => .. ( fr (fun z => fb b) ) .. ) )
(existT _ x .. (existT _ z tt) .. )
) ..
)
) (at level 85, x binder, z binder).
Check fun '((y,z):nat*nat) => pack (fr (fun '((y,z):nat*nat) => fb tt))
(existT _ (y,z) tt).
Example test := tele (t : Type) := tt.
Example test' := test nat.
Print test.
Example test2 := tele (t : Type) (x:t) := tt.
Example test2' := test2 nat 0.
Print test2.
Example test3 := tele (t : Type) (y:=0) (x:t) := tt.
Example test3' := test3 nat 0.
Print test3.
Example test4 := tele (t : Type) '((y,z):nat*nat) (x:t) := tt.
Example test4' := test4 nat (1,2) 3.
Print test4.
|
