diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-01 14:02:00 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-01 14:56:37 +0100 |
| commit | 3896701f162a5b6fb2923ebe3fee5066f74f2b5c (patch) | |
| tree | 29b2dbc6063e473956f5ab203712ab6c07440f38 | |
| parent | f19665eac65f9a37dcde85eb58e7d4b5b4a22bcf (diff) | |
Define well-formed thinnings.
| -rw-r--r-- | src/Core/Declarative.idr | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/src/Core/Declarative.idr b/src/Core/Declarative.idr index 4a27923..319b465 100644 --- a/src/Core/Declarative.idr +++ b/src/Core/Declarative.idr @@ -141,12 +141,23 @@ data TermConv where --- TermConv env (App t a) (App u b) (subst g $ sub1 a) -%name EnvWf wf +%name EnvWf envWf %name TypeWf wf %name TypeConv conv %name TermWf wf %name TermConv conv +public export +data ThinWf : sx `Thins` sy -> Env sy -> Env sx -> Type where + IdWf : ThinWf (id sx) env env + DropWf : ThinWf thin env2 env1 -> ThinWf (drop thin n) (Add env2 thin' a) env1 + KeepWf : + ThinWf thin env2 env1 -> + {auto 0 prf : IsNotId thin} -> + ThinWf (keep thin n) (Add env2 (thin . thin') a) (Add env1 thin' a) + +%name ThinWf thinWf + -- Well Formed Environment ----------------------------------------------------- typeWfImpliesEnvWf : TypeWf env a -> EnvWf env |