diff options
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 |