blob: f13cde3289b06abb5ab935bae98cdcbbb83932e5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
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 _)
|
