diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2024-10-30 16:09:58 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2024-10-30 16:09:58 +0000 |
| commit | 66169116cbacff64950407086fd0d832516a5f21 (patch) | |
| tree | 0b7249acd640941348684ce23f2d610cafca1779 /src/Inky.idr | |
| parent | 82783476f330801b54402bdcc4723add44a963dc (diff) | |
Define well-formedness for types.
Diffstat (limited to 'src/Inky.idr')
| -rw-r--r-- | src/Inky.idr | 4 |
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 () |