blob: bd374328f49824a21236948b3094636fc5256229 (
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
|
module Core.Declarative.Substitution
import Core.Context
import Core.Declarative
import Core.Environment
import Core.Thinning
import Core.Term
import Core.Term.Substitution
-- Definition ------------------------------------------------------------------
public export
data SubstWf : Env sy -> Subst sx sy -> Env sx -> Type where
Base : IsExtension thin env2 env1 -> SubstWf env2 (Base thin) env1
(:<) :
SubstWf env2 sub env1 ->
TermWf env2 (expand t) (expand a) ->
SubstWf env2 (sub :< t) (Add env1 a)
namespace Conv
public export
data SubstConv : Env sy -> Subst sx sy -> Subst sx sy -> Env sx -> Type where
Base : IsExtension thin env2 env1 -> SubstConv env2 (Base thin) (Base thin) env1
(:<) :
forall sub1, sub2.
SubstConv env2 sub1 sub2 env1 ->
TermConv env2 (expand t) (expand u) (expand a) ->
SubstConv env2 (sub1 :< t) (sub2 :< u) (Add env1 a)
|
