diff --git a/src/Quox/Lexer.idr b/src/Quox/Lexer.idr
index d2baaa0..7e11b4e 100644
--- a/src/Quox/Lexer.idr
+++ b/src/Quox/Lexer.idr
@@ -5,6 +5,8 @@ import Quox.Error
 import Data.String
 import public Text.Lexer
 
+%default total
+
 
 public export
 record Error where
diff --git a/src/Quox/NatExtra.idr b/src/Quox/NatExtra.idr
index f17179f..9e7d5de 100644
--- a/src/Quox/NatExtra.idr
+++ b/src/Quox/NatExtra.idr
@@ -2,6 +2,8 @@ module Quox.NatExtra
 
 import public Data.Nat
 
+%default total
+
 
 public export
 data LTE' : Nat -> Nat -> Type where
diff --git a/src/Quox/OPE.idr b/src/Quox/OPE.idr
index b3a381d..0f50df0 100644
--- a/src/Quox/OPE.idr
+++ b/src/Quox/OPE.idr
@@ -6,6 +6,8 @@ import Quox.NatExtra
 
 import Data.Nat
 
+%default total
+
 
 public export
 data OPE : Nat -> Nat -> Type where
diff --git a/src/Quox/Reduce.idr b/src/Quox/Reduce.idr
index 50f4038..8e25794 100644
--- a/src/Quox/Reduce.idr
+++ b/src/Quox/Reduce.idr
@@ -2,6 +2,8 @@ module Quox.Reduce
 
 import public Quox.Syntax
 
+%default total
+
 
 public export
 data IsRedexT : Term d n -> Type where
diff --git a/src/Quox/Syntax/Qty.idr b/src/Quox/Syntax/Qty.idr
index cea9af9..652b1e0 100644
--- a/src/Quox/Syntax/Qty.idr
+++ b/src/Quox/Syntax/Qty.idr
@@ -4,6 +4,8 @@ import Quox.Pretty
 
 import Data.Fin
 
+%default total
+
 
 public export
 data Qty = Zero | One | Any
diff --git a/src/Quox/Syntax/Term/Pretty.idr b/src/Quox/Syntax/Term/Pretty.idr
index 59d0578..1386cd2 100644
--- a/src/Quox/Syntax/Term/Pretty.idr
+++ b/src/Quox/Syntax/Term/Pretty.idr
@@ -7,6 +7,7 @@ import Quox.Pretty
 
 import Data.Vect
 
+%default total
 
 
 parameters {auto _ : Pretty.HasEnv m}
diff --git a/src/Quox/Syntax/Term/Reduce.idr b/src/Quox/Syntax/Term/Reduce.idr
index 267304a..f0266ef 100644
--- a/src/Quox/Syntax/Term/Reduce.idr
+++ b/src/Quox/Syntax/Term/Reduce.idr
@@ -3,6 +3,8 @@ module Quox.Syntax.Term.Reduce
 import Quox.Syntax.Term.Base
 import Quox.Syntax.Term.Subst
 
+%default total
+
 
 mutual
   ||| true if a term has a closure or dimension closure at the top level,
diff --git a/src/Quox/Syntax/Term/Subst.idr b/src/Quox/Syntax/Term/Subst.idr
index 1b76225..8e48065 100644
--- a/src/Quox/Syntax/Term/Subst.idr
+++ b/src/Quox/Syntax/Term/Subst.idr
@@ -2,6 +2,8 @@ module Quox.Syntax.Term.Subst
 
 import Quox.Syntax.Term.Base
 
+%default total
+
 
 export FromVar (Elim d) where fromVar = B
 export FromVar (Term d) where fromVar = E . fromVar