diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-06-01 17:07:41 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-06-01 17:07:41 +0100 |
| commit | d5f8497dbb6de72d9664f48d6acbc9772de77be3 (patch) | |
| tree | e1a4aeb598d263af3d888f8c0c68c07f15d13f14 /src/Total/NormalForm.idr | |
| parent | 3eb03e2347b35432f7eae7d6847ec9ecf1dff19e (diff) | |
Give a logical relation template.
Diffstat (limited to 'src/Total/NormalForm.idr')
| -rw-r--r-- | src/Total/NormalForm.idr | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/Total/NormalForm.idr b/src/Total/NormalForm.idr index 7421ca9..93a1da7 100644 --- a/src/Total/NormalForm.idr +++ b/src/Total/NormalForm.idr @@ -3,6 +3,8 @@ module Total.NormalForm import Total.Reduction import Total.Term +%prefix_record_projections off + public export data Neutral : Term ctx ty -> Type public export @@ -22,6 +24,7 @@ data Normal where %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 |