summaryrefslogtreecommitdiff
path: root/src/Obs/Substitution.idr
diff options
context:
space:
mode:
Diffstat (limited to 'src/Obs/Substitution.idr')
-rw-r--r--src/Obs/Substitution.idr2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Obs/Substitution.idr b/src/Obs/Substitution.idr
index 914e612..54df355 100644
--- a/src/Obs/Substitution.idr
+++ b/src/Obs/Substitution.idr
@@ -2,6 +2,8 @@ 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