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