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

• b6264f388d fix #11 the easy way rhiannon morris 2023-07-17 03:50:16 +0200
• 756fc60030 wip 🥚🛁 rhiannon morris 2023-07-12 22:56:35 +0200
• 612fb33663 bump again rhiannon morris 2023-07-13 21:28:39 +0200
• 30fbb40399 bitwise visibilities rhiannon morris 2023-06-24 14:35:59 +0200
• 124637c946 add SnocVect.select rhiannon morris 2023-06-24 14:28:08 +0200
• 33abbf659e remove stray comment rhiannon morris 2023-06-24 14:27:23 +0200
• 326db52204 more nat bitwise ops rhiannon morris 2023-06-24 14:27:09 +0200
• ddfbca7fcc (n-ary) coprod rhiannon morris 2023-06-05 17:25:02 +0200
• aca953c518 wip maybe.quox rhiannon morris 2023-06-05 16:42:11 +0200
• b61ace9c7d some bitwise ops corresponding to OPE ops rhiannon morris 2023-06-05 16:41:40 +0200
• 9e702dd03d switch syntax to codb rhiannon morris 2023-06-05 16:40:55 +0200
• 92870fe716 split and extend Quox.Thin rhiannon morris 2023-06-05 16:19:52 +0200
• a7673f901f add Quox.Thin rhiannon morris 2023-05-30 14:55:21 +0200
• 5580f90e8d add egtbs to bib rhiannon morris 2023-05-25 18:46:53 +0200
• fa09aaf228 squash warnings rhiannon morris 2023-06-23 18:32:05 +0200
• 6eccfeef52 pack bump rhiannon morris 2023-06-23 18:14:30 +0200
• f0d3529f63 fix subtype stuff for Eq rhiannon morris 2023-06-22 22:20:12 +0200
• cd330c1092 remove a noLoc rhiannon morris 2023-06-11 19:25:38 +0200
• 865772d512 remove stale todos rhiannon morris 2023-06-11 19:25:32 +0200
• 00e79d4264 quote names in Show rhiannon morris 2023-05-25 18:34:13 +0200
• a11bedd62a update pack rhiannon morris 2023-05-23 18:30:51 +0200
• c5fa11bdec don't need this agda file any more rhiannon morris 2023-05-23 18:30:44 +0200
• 4aa3e5f730 some modal type bibs rhiannon morris 2023-05-23 18:09:25 +0200
• 3bbf0366c8 make 0 in ★₀ optional rhiannon morris 2023-05-21 20:33:42 +0200
• 7c68cd9098 multimodal type theory bib rhiannon morris 2023-05-21 20:11:20 +0200
• 282565c7a3 Whnf ⇒ CanWhnf; WhnfM ⇒ Eff Whnf rhiannon morris 2023-05-21 20:11:01 +0200
• 2af8ee20ea those were not meant to stay there rhiannon morris 2023-05-21 20:10:09 +0200
• 42aa07c9c8 crude but effective stratification rhiannon morris 2023-05-21 20:09:34 +0200
• e4a20cc632 remove redundancy in equality check rhiannon morris 2023-05-20 21:38:23 +0200
• 64de93a13c remove square brackets around type lines rhiannon morris 2023-05-16 18:14:42 +0200
• d631b86be3 make p,q in coe/comp optional and default to @0 @1 rhiannon morris 2023-05-15 19:57:10 +0200
• 7b93a913c7 rewrite pretty printer rhiannon morris 2023-05-14 19:58:46 +0200
• f6abf084b3 qty lub is total actually (usually ω) rhiannon morris 2023-05-12 17:28:29 +0200
• ba755a9c4b haha oops rhiannon morris 2023-05-02 23:08:49 +0200
• 8d6ae6cc32 move location to the start of type errors rhiannon morris 2023-05-02 19:03:05 +0200
• d5f4a012c5 add source locations to inner syntax rhiannon morris 2023-05-02 03:06:25 +0200
• 30fa93ab4e refactor core syntax slightly to derive Eq/Show rhiannon morris 2023-04-27 21:37:20 +0200
• 7e079a9668 add file locations to Parser.Syntax rhiannon morris 2023-04-26 02:47:42 +0200
• 97f51b4436 all.quox rhiannon morris 2023-04-26 02:47:02 +0200
• b5f42cde64 remove big mutual blocks in parser rhiannon morris 2023-04-26 02:23:59 +0200
• adebfe090c error message tweaks rhiannon morris 2023-04-24 23:19:15 +0200
• b74ffa0077 rewrite parser rhiannon morris 2023-04-24 22:25:00 +0200
• 6c3b82ca64 ebnf syntax rhiannon morris 2023-04-23 17:33:50 +0200
• 0a06ea1280 fix qtys on nat.eqb rhiannon morris 2023-04-23 17:33:32 +0200
• a4ffd74625 fix the most embarrassing quantity mistake ever rhiannon morris 2023-04-20 19:29:57 +0200
• 3f06e8d68b allow multiple names in a binder rhiannon morris 2023-04-19 21:36:57 +0200
• b4a8438434 examples rhiannon morris 2023-04-19 00:42:40 +0200
• b666bc20cf do scope checking in FromParser where it belongs rhiannon morris 2023-04-18 22:55:23 +0200
• 55c0bf9974 fix skipping files rhiannon morris 2023-04-17 23:59:02 +0200
• 4578b30c79 namespaces work now rhiannon morris 2023-04-17 23:58:24 +0200
• 4db373a84f use constraints when checking δ rhiannon morris 2023-04-17 21:55:12 +0200
• ac85dc9352 don't put a ∷ℕ on nat literals that's silly rhiannon morris 2023-04-17 21:45:36 +0200
• 06b159973f pretty printing fixes rhiannon morris 2023-04-17 21:45:05 +0200
• 4ca32928fe examples rhiannon morris 2023-04-17 21:44:16 +0200
• c04c2e677c print quantity before names in main rhiannon morris 2023-04-17 21:43:53 +0200
• 682965eebd 0∨1 is not undefined it's ω rhiannon morris 2023-04-17 21:41:10 +0200
• 6428d39ce1 semicolons between decls in namespaces rhiannon morris 2023-04-17 21:41:00 +0200
• 3fb8580f85 re-add tightening and use it when messing with scopes rhiannon morris 2023-04-17 20:56:31 +0200
• a5ccf0215a coercions and compositions rhiannon morris 2023-04-15 15:13:01 +0200
• 468ae7e444 qiits using containers paper rhiannon morris 2023-04-15 14:15:07 +0200
• a42e82c355 type-case rhiannon morris 2023-04-03 17:46:23 +0200
• 868550327c print ':' on same line as name always rhiannon morris 2023-04-03 16:08:10 +0200
• 29505cbc06 examples/misc.quox rhiannon morris 2023-04-03 16:07:51 +0200
• 1211272420 factor out some pretty printing stuff rhiannon morris 2023-04-02 15:50:56 +0200
• e1dbf272df rename EqualE to just Equal & add runEqual rhiannon morris 2023-04-02 15:25:59 +0200
• 38dbd275a1 add case0 to syntax since that is possible sometimes rhiannon morris 2023-04-02 15:22:39 +0200
• 3f3079c48d bib: crude but effective stratification rhiannon morris 2023-04-01 22:33:40 +0200
• 308834a1c0 3 more tests rhiannon morris 2023-04-01 22:07:01 +0200
• ba2818a865 remove IsQty interface rhiannon morris 2023-04-01 19:16:43 +0200
• 5fdba77d04 nat example rhiannon morris 2023-04-01 19:16:30 +0200
• 924fd991f9 fix equality types rhiannon morris 2023-04-01 16:02:02 +0200
• 15f6f4c8a4 fix nat elim quantities rhiannon morris 2023-04-01 16:01:53 +0200
• 036e2bd4a5 fix case-box typing rhiannon morris 2023-04-01 16:01:29 +0200
• 1fce4d80f6 add box patterns to the parser oops rhiannon morris 2023-04-01 15:59:16 +0200
• a17752f31c fix up tests rhiannon morris 2023-03-31 23:43:25 +0200
• 5e220da2f4 a half-implemented verified dimeq rhiannon morris 2023-03-31 19:34:24 +0200
• 1ab0e42605 print a slightly better error if 'case' has no qty rhiannon morris 2023-03-31 19:33:40 +0200
• 13e9285bec some examples [that don't work yet] rhiannon morris 2023-03-31 19:31:49 +0200
• 64ac16c9f9 executable that typechecks files!! rhiannon morris 2023-03-31 19:31:29 +0200
• c8fbd73ea4 use names when pretty printing contexts rhiannon morris 2023-03-31 19:30:55 +0200
• ad942b2fd8 printing for most of FromParserError rhiannon morris 2023-03-31 19:27:38 +0200
• 2b2f79fca9 fix some typing mistakes rhiannon morris 2023-03-31 19:26:55 +0200
• 36609713ac mtl ⇒ eff rhiannon morris 2023-03-31 19:23:30 +0200
• 8a9b4c23dd box type rhiannon morris 2023-03-31 19:11:35 +0200
• 37dd1ee76d a few tests rhiannon morris 2023-03-27 00:08:48 +0200
• 7d36a7ff54 allow matching at 0 where appropriate rhiannon morris 2023-03-27 00:08:09 +0200
• 137962c176 add missing %default total rhiannon morris 2023-03-27 00:07:39 +0200
• 773f6372ea quantities in case don't need to be *exactly* the same rhiannon morris 2023-03-27 00:01:32 +0200
• f620dda639 fix error message rhiannon morris 2023-03-26 16:15:30 +0200
• 5df2a4538c more tests rhiannon morris 2023-03-26 16:15:19 +0200
• 5560cb6708 move 'enum' to Syntax.Base rhiannon morris 2023-03-26 16:14:58 +0200
• e6c4203b46 print ; between case branches rhiannon morris 2023-03-26 16:13:36 +0200
• 46e13c8ca2 don't print empty contexts in errors rhiannon morris 2023-03-26 16:10:39 +0200
• 84e1cc78cc use a SnocVect for subN rhiannon morris 2023-03-26 16:09:47 +0200
• 8402da6d5e dimeq test printing fix rhiannon morris 2023-03-26 14:45:32 +0200
• 7e3a8e72bd clean up printing of contexts rhiannon morris 2023-03-26 14:41:36 +0200
• 78e48911d0 check that an enum case head has the right type rhiannon morris 2023-03-26 14:41:17 +0200
• 9250789219 natural numbers rhiannon morris 2023-03-26 14:40:54 +0200
• fae534dae0 tweaks in equality checking rhiannon morris 2023-03-26 14:38:37 +0200
• 5053e9b234 remove inject stuff rhiannon morris 2023-03-25 22:41:30 +0100