From 66169116cbacff64950407086fd0d832516a5f21 Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Wed, 30 Oct 2024 16:09:58 +0000 Subject: Define well-formedness for types. --- src/Inky.idr | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/Inky.idr') 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 () -- cgit v1.2.3