diff options
| -rw-r--r-- | obs.ipkg | 1 | ||||
| -rw-r--r-- | src/Obs/Substitution.idr | 11 |
2 files changed, 12 insertions, 0 deletions
@@ -12,5 +12,6 @@ modules , Obs.Main , Obs.Parser , Obs.Sort + , Obs.Substitution , Obs.Syntax , Obs.Term 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 |