summaryrefslogtreecommitdiff
path: root/src/Inky.idr
diff options
context:
space:
mode:
Diffstat (limited to 'src/Inky.idr')
-rw-r--r--src/Inky.idr4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Inky.idr b/src/Inky.idr
index 40e9286..0c4db56 100644
--- a/src/Inky.idr
+++ b/src/Inky.idr
@@ -54,8 +54,8 @@ parseTerm toks = do
checkType : HasErr String es => Ty [<] -> App es ()
checkType a = do
- let False `Because` wf = illFormed a
- | True `Because` bad => throw "type ill-formed"
+ let True `Because` wf = wellFormed a
+ | False `Because` bad => throw "type ill-formed"
pure ()
checkTerm : (a : Ty [<]) -> (t : Term m [<] [<]) -> HasErr (NotChecks [<] [<] a t) es => App es ()