diff options
Diffstat (limited to 'src/Obs/Substitution.idr')
| -rw-r--r-- | src/Obs/Substitution.idr | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/Obs/Substitution.idr b/src/Obs/Substitution.idr new file mode 100644 index 0000000..914e612 --- /dev/null +++ b/src/Obs/Substitution.idr @@ -0,0 +1,11 @@ +module Obs.Substitution + +import Data.Fin + +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 |