blob: 93a1da748765b6c3211db4c339581ea5591d71ee (
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
|
module Total.NormalForm
import Total.Reduction
import Total.Term
%prefix_record_projections off
public export
data Neutral : Term ctx ty -> Type
public export
data Normal : Term ctx ty -> Type
data Neutral where
Var : Neutral (Var i)
App : Neutral t -> Normal u -> Neutral (App t u)
Rec : Neutral t -> Normal u -> Normal v -> Neutral (Rec t u v)
data Normal where
Ntrl : Neutral t -> Normal t
Abs : Normal t -> Normal (Abs t)
Zero : Normal Zero
Suc : Normal t -> Normal (Suc t)
%name Neutral n, m, k
%name Normal n, m, k
public export
record NormalForm (0 t : Term ctx ty) where
constructor MkNf
term : Term ctx ty
0 steps : t >= term
0 normal : Normal term
%name NormalForm nf
|
