diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2022-12-17 17:36:21 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2022-12-17 17:37:02 +0000 |
| commit | 6b7f7a0ad56a9500f592180c7b7c91b2b6a9acb9 (patch) | |
| tree | 947b70d49e4c0532ff57d1c46ce40456ba258bcb | |
| parent | 232857131888607ee3cd2ae4a5ccdc14e0c6f015 (diff) | |
Define substitution interfaces.
| -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 |