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

• 846bbc9ca3 more tc tests rhiannon morris 2023-02-13 22:06:53 +0100
• 534e0d2270 return () from check0 rhiannon morris 2023-02-13 22:06:03 +0100
• fe8c224299 write quantities before names in binders again rhiannon morris 2023-02-13 22:05:27 +0100
• a6f43a772e more equality & tests rhiannon morris 2023-02-12 21:30:08 +0100
• 3b9da2a1e5 update TAP rhiannon morris 2023-02-11 23:38:05 +0100
• 7d2c3b5a8e more typed equality, uip, etc rhiannon morris 2023-02-11 18:15:50 +0100
• 7fd7a31635 write variables as #𝑖 rhiannon morris 2023-02-11 18:14:31 +0100
• ac0334ca4c reexport needed types from Term.Split rhiannon morris 2023-02-11 18:14:12 +0100
• 8de5803cba add Context.unzip rhiannon morris 2023-02-11 18:13:44 +0100
• 42798f243f typed equality rhiannon morris 2023-02-10 21:40:44 +0100
• 3b13f0a82c silence a warning rhiannon morris 2023-02-02 14:58:36 +0100
• 4b36d8b7c8 pair stuff rhiannon morris 2023-01-26 19:54:46 +0100
• 6073ab4705 replace Split stuff with bools rhiannon morris 2023-01-23 03:39:46 +0100
• f0f49d9abf ScopeTerms that can bind multiple vars rhiannon morris 2023-01-23 03:22:50 +0100
• 92617a2e4a whnf actually reduces to whnf now (probably) rhiannon morris 2023-01-23 00:53:34 +0100
• f097e1c091 start of equality type stuff rhiannon morris 2023-01-21 02:34:28 +0100
• 8acc3aeadf visibility fix rhiannon morris 2023-01-21 01:41:30 +0100
• 8a2eea22fb make Definitions.isZero a predicate rhiannon morris 2023-01-21 01:41:21 +0100
• 1dc0c913e7 mugen in bib rhiannon morris 2023-01-18 21:24:45 +0100
• b25e5320d9 some more properties of var rhiannon morris 2023-01-12 16:03:09 +0100
• ef8b8b0da3 index Var.Compare by compare rhiannon morris 2023-01-10 00:08:47 +0100
• f405aeb7f9 simplify some matches rhiannon morris 2023-01-09 23:45:21 +0100
• 82795e9976 remove IsOne stuff; add timesSubj rhiannon morris 2023-01-09 23:43:55 +0100
• 28055c0f39 add Decidable-related stuff rhiannon morris 2023-01-09 23:43:23 +0100
• 84e524c978 make typechecker actually pass the dimeq to subT rhiannon morris 2023-01-09 19:03:21 +0100
• d8df40ab39 β↘↙ test rhiannon morris 2023-01-08 21:46:26 +0100
• c45a963ba0 parameterise over qty semiring rhiannon morris 2023-01-08 20:44:25 +0100
• 961c8415b5 a skipped η test rhiannon morris 2023-01-08 15:44:29 +0100
• 28eb99c091 style tweaks rhiannon morris 2023-01-08 15:44:20 +0100
• 0c1b3a78c3 remove ope stuff too rhiannon morris 2023-01-08 15:43:54 +0100
• 9dbd0b066c AnyTerm.(.def) => (.get) rhiannon morris 2023-01-08 15:07:01 +0100
• 98fa8d9967 mode eq mode into a reader rhiannon morris 2023-01-08 14:59:25 +0100
• 8443b2f6d8 remove lex/parse stuff for now rhiannon morris 2023-01-08 14:58:18 +0100
• 44c4aea06c nix flake update rhiannon morris 2023-01-07 14:06:19 +0100
• 5e11433c9f bit mask OPE stuff ope rhiannon morris 2022-11-15 15:44:49 +0100
• 42acbfc4ac rename SubView to Sub (Sub to Sub') and port over props rhiannon morris 2022-11-06 18:35:42 +0100
• 8582862914 remove stdlib duplication rhiannon morris 2022-11-06 13:03:54 +0100
• 5c3f2510fe split OPE stuff into modules rhiannon morris 2022-11-06 12:39:33 +0100
• 4b64399891 bitmask representation of lte rhiannon morris 2022-11-05 22:08:57 +0100
• 53bbcbf8c7 OPE & scope stuff rhiannon morris 2022-10-10 17:30:46 +0200
• 23c008b57a %inline rhiannon morris 2022-11-01 21:07:52 +0100
• e7272333cb remove a believe_me rhiannon morris 2022-11-01 21:05:04 +0100
• e1a9d99514 idris 0.6.0 [with temporary flake fork] rhiannon morris 2022-10-30 18:04:09 +0100
• 014de47a4c flake fix rhiannon morris 2022-10-30 13:26:44 +0100
• 881b22eee6 %inline rhiannon morris 2022-11-01 21:07:52 +0100
• 68dd93c02e remove a believe_me rhiannon morris 2022-11-01 21:05:04 +0100
• ad794d4441 idris 0.6.0 [with temporary flake fork] rhiannon morris 2022-10-30 18:04:09 +0100
• 72c25ad5e7 flake fix rhiannon morris 2022-10-30 13:26:44 +0100
• c8187c0801 OPE & scope stuff rhiannon morris 2022-10-10 17:30:46 +0200
• 8c05957f60 flake stuff rhiannon morris 2022-10-06 21:16:54 +0200
• 8a55cc9581 unfold definitions in equality checking, plus cleanup rhiannon morris 2022-08-23 05:43:23 +0200
• 44778825c2 add Definitions module rhiannon morris 2022-08-22 10:17:08 +0200
• 413c454898 pretty print E constructor as [brackets] rhiannon morris 2022-08-22 10:08:18 +0200
• 6dd18d89bd Uninhabited instances rhiannon morris 2022-08-22 10:07:46 +0200
• 77e94a3033 oops Shift.drop1 and ssDown were the same rhiannon morris 2022-06-24 11:28:25 +0200
• 956c677614 nix flake update rhiannon morris 2022-08-18 00:23:17 +0200
• 220a87f8a6 messing with nix again rhiannon morris 2022-06-19 14:22:58 +0200
• da91f7d95e a few more tests rhiannon morris 2022-05-27 18:00:06 +0200
• cd651558a2 idris doesn't support ARM i don't think rhiannon morris 2022-05-27 17:22:33 +0200
• 9920bea6e3 nix stuff rhiannon morris 2022-05-26 19:00:08 +0200
• b4ac58f866 move TAP to its own package rhiannon morris 2022-05-26 16:25:56 +0200
• 4befbbeb42 rename devShells after subdirs rhiannon morris 2022-05-26 12:32:42 +0200
• bc9344c6ba some reduction tests & fixes rhiannon morris 2022-05-25 16:10:19 +0200
• bd57a976a8 haha oops forgot some \{} rhiannon morris 2022-05-25 16:09:54 +0200
• 221b69e8e8 tweak test formatting rhiannon morris 2022-05-25 16:05:20 +0200
• de3e13bad8 support notes/comments in test output rhiannon morris 2022-05-25 16:04:51 +0200
• 2b756ae1bb tiny tweak rhiannon morris 2022-05-25 16:03:23 +0200
• 818d559d58 shut up about dirty git trees rhiannon morris 2022-05-25 16:01:54 +0200
• 3cf246b4dc merge Quox.{Syntax.Term.}Reduce rhiannon morris 2022-05-25 15:59:58 +0200
• b0692c15b9 fancier tests rhiannon morris 2022-05-24 12:09:17 +0200
• 25f9df34ab [bib] OTT for good rhiannon morris 2022-05-20 17:26:52 +0200
• cde2a9b0d6 derive impls where possible rhiannon morris 2022-05-13 07:05:55 +0200
• 274ecfb58c normalizeNfc rhiannon morris 2022-05-12 07:41:58 +0200
• c743a99356 char class stuff rhiannon morris 2022-05-10 22:40:44 +0200
• 123e4b6ab4 general categories rhiannon morris 2022-05-10 04:13:11 +0200
• 89f9793143 equality tests rhiannon morris 2022-05-09 18:31:43 +0200
• a26eba7d7f parser stuff rhiannon morris 2022-05-09 18:31:30 +0200
• 5b1dab24f2 𝒰 → ★ rhiannon morris 2022-05-09 04:30:37 +0200
• 50a2ec02cb parser stuff rhiannon morris 2022-05-08 20:03:05 +0200
• 8a955eebb3 some equality tests rhiannon morris 2022-05-08 20:02:57 +0200
• 756bc5b9f3 fromInteger for universe rhiannon morris 2022-05-08 20:02:21 +0200
• 41056559f2 add .#lib and .#test devShell aliases rhiannon morris 2022-05-08 19:29:03 +0200
• 77c1492cad add some missing --no-link flags rhiannon morris 2022-05-08 19:28:49 +0200
• 1e7a6cf01f parser stuff rhiannon morris 2022-05-08 05:41:55 +0200
• f5a98e6584 add impls of Eq/Show to Term/Elim in tests rhiannon morris 2022-05-08 05:41:32 +0200
• fcbc92e54c more tokens rhiannon morris 2022-05-07 21:57:10 +0200
• 12753eb894 adjust precedence of (:-) rhiannon morris 2022-05-07 21:30:41 +0200
• 809a0fc859 simplify lexical grammar rhiannon morris 2022-05-07 21:26:16 +0200
• 1c8b2b205b temp fix for nix flake show etc rhiannon morris 2022-05-07 17:37:47 +0200
• 3b13ec47f5 more parser tests rhiannon morris 2022-05-07 00:58:03 +0200
• 715a9fe8f9 Show for Name and Dim rhiannon morris 2022-05-07 00:57:23 +0200
• 804f1e3638 remove src directories rhiannon morris 2022-05-06 22:01:44 +0200
• 79211cff84 start of parser stuff rhiannon morris 2022-05-06 21:58:32 +0200
• d43a2429e1 makefile fixes rhiannon morris 2022-05-06 21:35:19 +0200
• 1dd4ff0e22 lex . and ω (and #) rhiannon morris 2022-05-06 21:35:04 +0200
• 49c43ad296 heartbreaking: Quox.Error doesn't actually work rhiannon morris 2022-05-06 21:23:58 +0200
• 944749d868 nix fixes (nixes) rhiannon morris 2022-05-06 20:27:45 +0200
• 1931f954fb renamings rhiannon morris 2022-05-04 20:13:56 +0200
• 8093e4108a make quox-exe the default package rhiannon morris 2022-05-04 19:26:30 +0200
• 5ee637cf4d update makefile rhiannon morris 2022-05-04 18:49:00 +0200