src/Obs/Substitution.idr


1
2
3
4
5
6
7
8
9
10
11
12
13

module Obs.Substitution

import Data.Fin

%default total

public export
interface Rename (x : Nat -> Type) where
  rename : forall m, n . x n -> (Fin n -> Fin m) -> x m

public export
interface Subst (x, y, z : Nat -> Type) where
  subst : forall m, n . x n -> (Fin n -> y m) -> z m