blob: 14a3f2036a34db7164d0e9a50f0eeafde61241bb (
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
|
module Core.Term.NormalForm
import Core.Context
import Core.Term
import Core.Var
-- Definition ------------------------------------------------------------------
public export
data Neutral : Term sx -> Type where
Var : Neutral (Var v)
App : Neutral t -> Neutral (App t u)
public export
data Whnf : Term sx -> Type where
Ntrl : Neutral t -> Whnf t
Set : Whnf Set
Pi : Whnf (Pi n t u)
Abs : Whnf (Abs n t)
%name Neutral n, m
%name Whnf n, m
|
