diff options
| -rw-r--r-- | obs.ipkg | 1 | ||||
| -rw-r--r-- | src/Core/Term/NormalForm.idr | 25 |
2 files changed, 26 insertions, 0 deletions
@@ -13,6 +13,7 @@ modules , Core.Reduction , Core.Term , Core.Term.Environment + , Core.Term.NormalForm , Core.Term.Substitution , Core.Thinning , Core.Var diff --git a/src/Core/Term/NormalForm.idr b/src/Core/Term/NormalForm.idr new file mode 100644 index 0000000..14a3f20 --- /dev/null +++ b/src/Core/Term/NormalForm.idr @@ -0,0 +1,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 |