summaryrefslogtreecommitdiff
path: root/src/Obs/Typing.idr
diff options
context:
space:
mode:
Diffstat (limited to 'src/Obs/Typing.idr')
-rw-r--r--src/Obs/Typing.idr2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Obs/Typing.idr b/src/Obs/Typing.idr
index 2a96a97..95ffc19 100644
--- a/src/Obs/Typing.idr
+++ b/src/Obs/Typing.idr
@@ -13,6 +13,8 @@ import Text.Bounded
import Text.PrettyPrint.Prettyprinter
import Text.PrettyPrint.Prettyprinter.Render.Terminal
+%default total
+
-- Conversion ------------------------------------------------------------------
-- invariant: all definitions fully expanded