blob: f4697f5d5a8500671f59b60208308ac8e8d30306 (
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
45
46
47
48
|
module NormalForm
import Data.SnocList.Elem
import Term
import Thinning
-- Neutrals and Normals --------------------------------------------------------
public export
data IsNeutral : Term ctx ty -> Type
public export
data IsNormal : Term ctx ty -> Type
data IsNeutral where
Var : IsNeutral (Var i)
App : IsNeutral t -> IsNormal u -> IsNeutral (App t u)
Rec : IsNeutral t -> IsNormal u -> IsNormal v -> IsNeutral (Rec t u v)
data IsNormal where
Ntrl : IsNeutral t -> IsNormal t
Abs : IsNormal t -> IsNormal (Abs t)
Zero : IsNormal Zero
Succ : IsNormal t -> IsNormal (Succ t)
%name IsNeutral prf
%name IsNormal prf
public export
record Normal (ctx : SnocList Ty) (ty : Ty) where
constructor MkNormal
forget : Term ctx ty
0 isNormal : IsNormal forget
%name Normal n, m, k
-- Inversions ------------------------------------------------------------------
export
predNorm : IsNormal (Succ t) -> IsNormal t
predNorm (Succ prf) = prf
export
appNtrl : IsNormal (App t u) -> IsNeutral (App t u)
appNtrl (Ntrl prf) = prf
export
recNtrl : IsNormal (Rec t u v) -> IsNeutral (Rec t u v)
recNtrl (Ntrl prf) = prf
|
