rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

recognise nats other than 0 in eq checker

Browse source
This commit is contained in:
rhiannon morris 2023-12-21 17:48:12 +01:00
parent 0fdd4741be
commit 7afcbfe258
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
lib/Quox/Equal.idr
View file

@ -305,10 +305,10 @@ namespace Term
(E _, Nat 0 {}) => clashT s.loc ctx nat s t (E _, Nat 0 {}) => clashT s.loc ctx nat s t
(E _, Succ {}) => clashT s.loc ctx nat s t (E _, Succ {}) => clashT s.loc ctx nat s t
(Nat 0 {}, t) => wrongType t.loc ctx nat t (Nat {}, t) => wrongType t.loc ctx nat t
(Succ {}, t) => wrongType t.loc ctx nat t (Succ {}, t) => wrongType t.loc ctx nat t
(E _, t) => wrongType t.loc ctx nat t (E _, t) => wrongType t.loc ctx nat t
(s, _) => wrongType s.loc ctx nat s (s, _) => wrongType s.loc ctx nat s
compare0' defs ctx sg str@(STRING {}) s t = local_ Equal $ compare0' defs ctx sg str@(STRING {}) s t = local_ Equal $
case (s, t) of case (s, t) of