Commit graph

Select branches

Hide pull requests

ope

qpoly

𝕎

🎋

🐉

🥚🛁

#12

#19

#25

#28

#29

#30

#35

#36

#39

#40

#42

#43

#44

#47

Mono Color

• 126a585c74 remove unused dep rhiannon morris 2023-03-25 20:55:47 +01:00
• 5945265867 some DimEq tests rhiannon morris 2023-03-25 20:55:28 +01:00
• 50c682f715 bump rhiannon morris 2023-03-25 20:54:47 +01:00
• 75376619f9 move pretty stuff for DimEq rhiannon morris 2023-03-25 20:54:31 +01:00
• ab73c474c3 add DimEq.wf and export some things to make it work rhiannon morris 2023-03-25 20:50:03 +01:00
• 5a994ac0e2 derive Eq,Ord,Show for DimEq rhiannon morris 2023-03-25 20:49:14 +01:00
• ab82883214 add weakD rhiannon morris 2023-03-25 20:48:49 +01:00
• 100063ab91 add runPrettyWith, etc rhiannon morris 2023-03-25 20:48:26 +01:00
• 60079d9eb9 update for tap update rhiannon morris 2023-03-25 20:42:44 +01:00
• 443da20c4b print non-dependent function types as "π.A → B" rhiannon morris 2023-03-18 23:32:53 +01:00
• 8f0f0c1891 "1.(x: A) → B" instead of "(1.x: A) → B" rhiannon morris 2023-03-18 23:27:27 +01:00
• ebf6aefb1d parser tweaks rhiannon morris 2023-03-18 20:00:29 +01:00
• 51468f54fc misc parse/print tests rhiannon morris 2023-03-18 02:47:15 +01:00
• ea24d00544 print non-dependent products (easy mode) rhiannon morris 2023-03-18 02:46:19 +01:00
• 958bc2f8b8 quote tags in printing if they're not identifiers rhiannon morris 2023-03-18 02:45:30 +01:00
• f2272da4b4 replace '≔' and '·' with '=' and (only) '.' rhiannon morris 2023-03-17 21:54:09 +01:00
• 1c53b63bdf uh. fix Tests.Lexer rhiannon morris 2023-03-17 21:51:28 +01:00
• 8cf260ee2e reorder some imports rhiannon morris 2023-03-17 21:50:04 +01:00
• f814b01c5c quote tags in printer when needed rhiannon morris 2023-03-16 18:39:24 +01:00
• be94422668 move name lexing stuff to Quox.Name rhiannon morris 2023-03-16 18:34:49 +01:00
• b9825fee55 ?????? rhiannon morris 2023-03-16 18:20:33 +01:00
• f5fa63a6df some pretty printing tests rhiannon morris 2023-03-16 18:19:17 +01:00
• 6dc7177be5 use NContext/SnocVect for scope name lists etc rhiannon morris 2023-03-16 18:18:49 +01:00
• 32f38238ef pretty printing errors rhiannon morris 2023-03-15 15:54:51 +01:00
• 54ba4e237f use snoclists in pretty printing rhiannon morris 2023-03-15 15:53:39 +01:00
• c9b9f66693 rename 'prettyTerm' to 'prettyIO' rhiannon morris 2023-03-15 15:42:28 +01:00
• 86d21caf24 put names into contexts, and contexts into errors rhiannon morris 2023-03-14 03:22:26 +01:00
• f4af1a5a78 split up Quox.Typing rhiannon morris 2023-03-13 21:41:57 +01:00
• ecd3be8bda "WhnfErr" ⇒ "WhnfError" rhiannon morris 2023-03-13 19:39:29 +01:00
• 765c62866a more FromParser rhiannon morris 2023-03-13 19:33:09 +01:00
• 90232dd1f8 rename some things to get rid of warnings rhiannon morris 2023-03-13 19:32:52 +01:00
• 507eb79788 consistent indexing rhiannon morris 2023-03-13 19:31:52 +01:00
• 7f46537cbc "abstract" ⇒ "postulate" rhiannon morris 2023-03-13 19:31:05 +01:00
• 8e9b0abb34 Show Telescope rhiannon morris 2023-03-13 18:25:07 +01:00
• c81aabcc14 more parser/FromParser stuff rhiannon morris 2023-03-12 18:28:37 +01:00
• cd63eb2c67 the "observational" here doesn't really say anything new rhiannon morris 2023-03-10 23:42:35 +01:00
• d9bc68446f more fromparser stuff rhiannon morris 2023-03-10 21:52:29 +01:00
• 426c138c2b clean up some old unused stuff rhiannon morris 2023-03-08 22:33:52 +01:00
• 88985405ce change some single-character constructor names rhiannon morris 2023-03-08 16:46:29 +01:00
• 47fca359f4 fix weird IsReserved issue rhiannon morris 2023-03-06 12:04:43 +01:00
• 757ea89b0f add definitions to parser rhiannon morris 2023-03-06 11:35:57 +01:00
• ab2508e0ce add fromPTerm, etc rhiannon morris 2023-03-05 16:49:50 +01:00
• b7acf39c39 remove universe type rhiannon morris 2023-03-05 16:48:29 +01:00
• 0cae84c75b add module Parser.Syntax with PTerm and toPTerm rhiannon morris 2023-03-05 14:55:04 +01:00
• 8fc0b414cf fix tag stuff in test labels rhiannon morris 2023-03-05 13:17:46 +01:00
• 02b94ab705 split check and checkType. UAny is kill rhiannon morris 2023-03-05 13:14:25 +01:00
• 21da2d1d21 add - as an idCont char rhiannon morris 2023-03-05 12:18:39 +01:00
• f6bc8cad1f add some dim app tests rhiannon morris 2023-03-05 12:18:15 +01:00
• edeee68cb7 parser rhiannon morris 2023-03-04 21:02:51 +01:00
• 95a6644a6c rename <&&>/<||> to andM/orM rhiannon morris 2023-03-03 12:19:15 +01:00
• 841564f69f fix typo in comment rhiannon morris 2023-03-02 19:56:22 +01:00
• 0a2d05818e fix fixities rhiannon morris 2023-03-02 19:56:16 +01:00
• fc3c2dc8ab sop → elab-util rhiannon morris 2023-03-02 19:52:32 +01:00
• 04d3c9368a replace nix with pack rhiannon morris 2023-03-02 19:51:25 +01:00
• dbe248be9a lexer rhiannon morris 2023-02-28 20:51:54 +01:00
• cacb3225a2 unicode stuff rhiannon morris 2023-02-27 07:27:27 +01:00
• 28356200c1 pretty printer refactoring rhiannon morris 2023-02-26 14:54:18 +01:00
• 75ef078b4b don't print substitutions by default rhiannon morris 2023-02-26 11:25:11 +01:00
• 8447098f28 look through substitutions in Q.S.T.Split rhiannon morris 2023-02-26 11:24:28 +01:00
• e896b24f58 print ` before enum types rhiannon morris 2023-02-26 11:23:30 +01:00
• eaf679edf7 print dimension app with an @ rhiannon morris 2023-02-26 11:22:44 +01:00
• ab63edf572 print bound vars as e.g. x#1 instead of x:1 rhiannon morris 2023-02-26 11:21:47 +01:00
• 4826c35ad6 rearrange some auto args for better overriding rhiannon morris 2023-02-26 11:21:25 +01:00
• 82a2f92ddf pprint universes as a direct suffix rhiannon morris 2023-02-26 11:20:06 +01:00
• fbfbe57266 change some highlighting rhiannon morris 2023-02-26 11:18:11 +01:00
• 60f07a938e move pushSubsts to Q.S.T.Subst rhiannon morris 2023-02-26 11:17:42 +01:00
• 55cdb19a4c replace ⇒ with . in lambdas, etc rhiannon morris 2023-02-26 11:01:47 +01:00
• 630832f6c7 tweak quog tongue rhiannon morris 2023-02-26 10:58:47 +01:00
• c25b910edf fix Main.idr rhiannon morris 2023-02-26 10:58:22 +01:00
• 79a828449a use ★ for Type in unicode mode rhiannon morris 2023-02-25 19:14:26 +01:00
• 4b284d6e01 rename λᴰ to δ rhiannon morris 2023-02-25 19:14:11 +01:00
• 302de6266e nicer constructors for ASTs rhiannon morris 2023-02-25 15:24:45 +01:00
• 3d9b730803 some more typechecker tests rhiannon morris 2023-02-23 10:04:16 +01:00
• 4b814d7502 fix quantity in CasePair typing rhiannon morris 2023-02-23 10:04:00 +01:00
• abe812fc40 update tap, also other flakes rhiannon morris 2023-02-23 10:02:45 +01:00
• efca9a7138 add enums, which also need whnf to be fallible :( rhiannon morris 2023-02-22 07:45:10 +01:00
• 0e481a8098 new representation for scopes rhiannon morris 2023-02-22 07:40:19 +01:00
• c75f1514ba add BoolExtra rhiannon morris 2023-02-22 05:42:56 +01:00
• 1a7efc104e Replace subst overloading with interfaces too (mostly) rhiannon morris 2023-02-20 22:22:23 +01:00
• cb5bd6c98c make overloaded reduce stuff into interfaces rhiannon morris 2023-02-20 21:42:31 +01:00
• 56791e286d make typechecker NotClo args implicit rhiannon morris 2023-02-20 21:42:21 +01:00
• f959dc28fe add Functor etc for IfConsistent rhiannon morris 2023-02-20 21:38:47 +01:00
• 7895fa37e5 Q.S.T.Reduce ⇒ Q.Reduce and make it use Definition directly rhiannon morris 2023-02-19 18:22:53 +01:00
• ae43c324c0 remove commented modules from ipkg rhiannon morris 2023-02-19 18:22:27 +01:00
• 876a45f565 fix "make clean" rhiannon morris 2023-02-19 18:21:52 +01:00
• 85a55f8123 wrap type errors in extra context rhiannon morris 2023-02-19 17:54:39 +01:00
• 858b5db530 check for 0=1 in typechecker rhiannon morris 2023-02-19 17:51:44 +01:00
• 195791e158 export isSubSing rhiannon morris 2023-02-19 17:43:27 +01:00
• 27e61011ac %inline rhiannon morris 2023-02-19 17:43:14 +01:00
• 810de09f61 zeroIsSubj/zeroIsGlobal work on all zeroes rhiannon morris 2023-02-19 17:42:11 +01:00
• e375d008e5 comments etc rhiannon morris 2023-02-19 17:04:57 +01:00
• d71ac8c34d rename Equal.Env to CmpContext rhiannon morris 2023-02-19 17:02:13 +01:00
• cba6dafc58 remove unused confusing ClashE rhiannon morris 2023-02-19 17:00:51 +01:00
• 9bfc82ca43 add a bib entry, update some links rhiannon morris 2023-02-19 16:14:19 +01:00
• f22f194dc5 add super counterparts to sub rhiannon morris 2023-02-14 22:29:06 +01:00
• bee6eeacdf pass a TyContext into equal etc, rather than its components rhiannon morris 2023-02-14 22:28:10 +01:00
• 065ebedf2d use DimEq directly in typing context rhiannon morris 2023-02-14 21:29:04 +01:00
• 4b7379f094 fix tiny bug in dimeq rhiannon morris 2023-02-14 21:28:50 +01:00
• 802dfae493 slight simplify rhiannon morris 2023-02-14 21:16:20 +01:00
• c40e6a60ff remove input qctx since it isn't used rhiannon morris 2023-02-14 21:14:47 +01:00