16 lines
385 B
Coq
16 lines
385 B
Coq
Inductive term: Type :=
|
||
| Var: nat -> term
|
||
| Abs: term -> term
|
||
| App: term -> term -> term.
|
||
|
||
Notation "'λ' body" := (Abs body) (at level 60, right associativity).
|
||
Notation "'❨' t1 t2 '❩'" := (App t1 t2) (at level 50).
|
||
Notation "'`' varidx " := (Var varidx) (at level 40).
|
||
|
||
Check λ`0.
|
||
Check λ❨`0 `0❩.
|
||
Check ❨λ❨`0 `0❩ λ❨`0 `0❩❩.
|
||
|
||
Require Import List.
|
||
Search In.
|