diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-16 15:25:02 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-16 15:25:02 +0100 |
| commit | cdcfdcd31ccfee2b2a491713b4527ca87dd586bf (patch) | |
| tree | ede7122da2d42d2c8d95eaa509e94fc269432407 /src/Core/Declarative.idr | |
| parent | dc9aa0cc59d67690e7eba1543a37c397e751429a (diff) | |
Define term reduction.
Diffstat (limited to 'src/Core/Declarative.idr')
| -rw-r--r-- | src/Core/Declarative.idr | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/Core/Declarative.idr b/src/Core/Declarative.idr index 38e6ccd..1292fc9 100644 --- a/src/Core/Declarative.idr +++ b/src/Core/Declarative.idr @@ -8,10 +8,15 @@ import Core.Thinning -- Definition ------------------------------------------------------------------ +public export data EnvWf : Env n -> Type +public export data TypeWf : Env n -> Term n -> Type +public export data TypeConv : Env n -> Term n -> Term n -> Type +public export data TermWf : Env n -> Term n -> Term n -> Type +public export data TermConv : Env n -> Term n -> Term n -> Term n -> Type data EnvWf where |