diff options
| -rw-r--r-- | obs.ipkg | 3 | ||||
| -rw-r--r-- | src/Core/Environment.idr | 40 |
2 files changed, 42 insertions, 1 deletions
@@ -7,7 +7,8 @@ depends = contrib options = "--total" modules - = Core.Term + = Core.Environment + , Core.Term , Core.Term.Substitution , Core.Term.Thinned , Core.Thinning diff --git a/src/Core/Environment.idr b/src/Core/Environment.idr new file mode 100644 index 0000000..f13cde3 --- /dev/null +++ b/src/Core/Environment.idr @@ -0,0 +1,40 @@ +module Core.Environment + +import Core.Term +import Core.Term.Thinned +import Core.Thinning + +infix 4 =~= + +-- Definition ------------------------------------------------------------------ + +public export +data Env : Nat -> Type where + Lin : Env 0 + (:<) : Env n -> Thinned n -> Env (S n) + +namespace Eq + public export + data (=~=) : Env n -> Env n -> Type where + Refl : env =~= env + (:<) : env1 =~= env2 -> t =~= u -> env1 :< t =~= env2 :< u + +%name Env env +%name Eq.(=~=) prf + +-- Indexing -------------------------------------------------------------------- + +public export +index : Env n -> Fin n -> Thinned n +index (env :< t) FZ = wkn t (drop $ id _) +index (env :< t) (FS i) = wkn (index env i) (drop $ id _) + +export +indexCong : + {0 env1, env2 : Env n} -> + env1 =~= env2 -> + (i : Fin n) -> + index env1 i =~= index env2 i +indexCong Refl i = Refl +indexCong (prf :< prf') FZ = wknCong prf' (drop $ id _) +indexCong (prf :< prf') (FS i) = wknCong (indexCong prf i) (drop $ id _) |