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)