From cdcfdcd31ccfee2b2a491713b4527ca87dd586bf Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Sun, 16 Apr 2023 15:25:02 +0100 Subject: Define term reduction. --- src/Core/Declarative.idr | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'src/Core/Declarative.idr') 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 -- cgit v1.2.3