diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Core/Term/Environment.idr | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/src/Core/Term/Environment.idr b/src/Core/Term/Environment.idr index 62e3b60..4f167f9 100644 --- a/src/Core/Term/Environment.idr +++ b/src/Core/Term/Environment.idr @@ -41,3 +41,20 @@ index : Env sx -> Var sx -> Term sx index env i = let MkRes val thin = doIndex env $ view i in wkn val thin + +-- Equality -------------------------------------------------------------------- + +namespace Eq + public export + data EnvEq : Env sx -> Env sx -> Type where + Lin : EnvEq [<] [<] + Add : + EnvEq env1 env2 -> + Term.wkn t thin1 = wkn u thin2 -> + EnvEq (Add env1 thin1 t) (Add env2 thin2 u) + + %name EnvEq prf + + public export + (:<) : EnvEq env1 env2 -> (0 t : Term sx) -> EnvEq (env1 :< t) (env2 :< t) + prf :< t = Add prf Refl |