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

• 2f8a2d2cd2 fix typo in error rhiannon morris 2023-11-04 17:45:55 +0100
• b6c435049d escape strings in scheme rhiannon morris 2023-11-03 20:08:45 +0100
• 90cdcfe4da add \n and \t escapes to the lexer rhiannon morris 2023-11-03 20:07:59 +0100
• d4639a35c6 add hello.quox to examples rhiannon morris 2023-11-03 17:42:59 +0100
• b7e1f37b5b add some #[compile-scheme] rhiannon morris 2023-11-03 17:42:44 +0100
• 5dfefe443c more tidying of outputs rhiannon morris 2023-11-03 17:42:07 +0100
• 0514fff481 represent ℕ constants directly rhiannon morris 2023-11-02 20:01:34 +0100
• fa7f82ae5a rename Nat to NAT in AST rhiannon morris 2023-11-02 18:14:22 +0100
• e0ed37720f always vsep scheme lets, otherwise they are unreadable rhiannon morris 2023-11-01 15:17:15 +0100
• 4cc50c6bcd highlight errors even if real output is to a file rhiannon morris 2023-11-01 14:16:03 +0100
• 050346e344 add postulate, #[compile-scheme], #[main] rhiannon morris 2023-11-01 12:56:27 +0100
• cc0bade747 scheme output rhiannon morris 2023-10-24 23:52:19 +0200
• cd08a0fd98 more erasure rhiannon morris 2023-10-24 23:50:28 +0200
• 1f14e4ab9e automate more option stuff rhiannon morris 2023-10-24 18:25:56 +0200
• 314e7f036d make nat elimination with erased IH non-recursive at runtime rhiannon morris 2023-11-03 17:48:12 +0100
• 6ab9637ab5 don't keep erased applications actually rhiannon morris 2023-11-03 17:47:55 +0100
• b6fd1e921e pretty printing improvements rhiannon morris 2023-11-03 17:47:01 +0100
• f4a45b6c52 keep the Except effect at the start of the list rhiannon morris 2023-11-03 17:45:02 +0100
• 8e0d66cab8 more erasure rhiannon morris 2023-10-21 20:49:29 +0200
• ea74c148b7 some of this EffExtra stuff doesn't work rhiannon morris 2023-10-21 20:48:28 +0200
• 83ab871d61 new main rhiannon morris 2023-10-20 17:42:01 +0200
• 421eb220fd erasure refactor rhiannon morris 2023-10-20 06:09:20 +0200
• fbb862c88b %default total rhiannon morris 2023-10-20 05:28:42 +0200
• b651ed5447 LoadFile does the parsing rhiannon morris 2023-10-20 05:23:56 +0200
• d6985cad55 tweak the pretty printer stuff slightly rhiannon morris 2023-10-20 04:53:49 +0200
• 52e54dcc3c add PrettyVal stuff for parser AST rhiannon morris 2023-10-20 04:53:20 +0200
• 0c1df54d62 improve handling of context lengths rhiannon morris 2023-10-15 16:23:38 +0200
• 2e9183bc14 add prettyDef rhiannon morris 2023-10-15 16:12:43 +0200
• 428397f42b erasure to untyped syntax rhiannon morris 2023-09-30 18:37:44 +0200
• 0b7bd0ef46 add locations and substitutions to untyped syntax rhiannon morris 2023-09-30 18:36:30 +0200
• 9cbd998d6f simplify isEmpty and isSubSing rhiannon morris 2023-09-30 18:32:26 +0200
• 6896c8fcc4 rename SQtys to sg (σ) rhiannon morris 2023-09-30 18:31:23 +0200
• be8797a3ef untyped λ calculus syntax rhiannon morris 2023-09-20 22:09:08 +0200
• bf605486f0 example updates rhiannon morris 2023-11-03 17:42:31 +0100
• 69f032584e fix constructor name in comment rhiannon morris 2023-11-02 18:14:28 +0100
• 9ecaaf72bd bump pack collection rhiannon morris 2023-10-21 20:46:35 +0200
• f04c4619ef detect reserved words inside names like 'a.λ.b' rhiannon morris 2023-09-24 17:36:20 +0200
• d4de74eab6 change it to #[..] since # is also reserved rhiannon morris 2023-09-22 18:38:40 +0200
• bcfb0d81b8 update tests rhiannon morris 2023-09-22 18:38:32 +0200
• 8395bec4cb check for duplicate cases in enum matches rhiannon morris 2023-09-22 14:03:00 +0200
• 6153b4f7f8 add a couple of failing examples rhiannon morris 2023-09-22 13:48:11 +0200
• d4cfbd4045 add @[fail] modifier to declarations rhiannon morris 2023-09-22 01:29:23 +0200
• ea674503c0 export PushSubsts, oops 🎋 rhiannon morris 2023-09-20 21:58:55 +0200
• b1eefb0f4d move prettyTag to Quox.Pretty rhiannon morris 2023-09-20 21:58:42 +0200
• ee22486e97 rename BindName.name to .val rhiannon morris 2023-09-20 21:58:27 +0200
• 08fb686bf6 move Scoped to separate module rhiannon morris 2023-09-20 21:58:04 +0200
• cf3ed604a4 move Quox.Syntax.Var to just Quox.Var rhiannon morris 2023-09-20 21:56:59 +0200
• 4704dd0441 remove on-hold dir rhiannon morris 2023-09-20 21:55:03 +0200
• dc076b636d fix warnings rhiannon morris 2023-09-19 18:05:43 +0200
• 80b1b3581a use ST from base rhiannon morris 2023-09-19 00:41:47 +0200
• ebde478adc add η for pairs in zero contexts rhiannon morris 2023-09-19 00:41:17 +0200
• bb8d2464af add fst and snd rhiannon morris 2023-09-18 21:52:51 +0200
• e6c06a5c81 pass the subject quantity through equality etc rhiannon morris 2023-09-18 18:21:30 +0200
• 3fe9b96f05 make function types with an empty domain subsingletons rhiannon morris 2023-09-17 20:09:33 +0200
• 244b33d786 fix some comments rhiannon morris 2023-09-17 19:10:52 +0200
• b85dcb5402 η for box rhiannon morris 2023-09-17 19:10:46 +0200
• e1257560b7 Show for contexts, etc rhiannon morris 2023-09-17 19:09:54 +0200
• ac518472ad bump pack db rhiannon morris 2023-09-17 19:09:10 +0200
• 4c88918ade stop throwing names away rhiannon morris 2023-09-17 19:06:07 +0200
• 7bd959e919 some example stuff rhiannon morris 2023-09-17 14:41:29 +0200
• 8221d71416 some refactors rhiannon morris 2023-09-17 13:54:26 +0200
• 7b53d56072 a few basic fv tests to make sure it's not reversed or whatever rhiannon morris 2023-09-16 13:34:11 +0200
• fa14ce1a02 add FreeVars, and split only on used dvars in Equal rhiannon morris 2023-09-12 09:56:49 +0200
• 9973f8d07b refactor elim equality error stuff rhiannon morris 2023-09-12 06:48:51 +0200
• 1e8932690b untangle big mutual block in Equal rhiannon morris 2023-08-28 22:07:33 +0200
• d5d30ee198 loosen pushCoe's type slightly rhiannon morris 2023-08-28 20:03:06 +0200
• add2eb400c make Elim.compare0 able to pass a type to isSubSing rhiannon morris 2023-08-28 20:00:54 +0200
• 6f9d31aa0a add displacement to Definition rhiannon morris 2023-08-28 19:59:36 +0200
• 6dcd3332c1 granule & defuncn bibs rhiannon morris 2023-08-28 19:57:28 +0200
• 32f6e5a3b1 make displace total (with a few asserts) rhiannon morris 2023-08-28 19:57:02 +0200
• 72609bc12f Elim.compare0 infers the type rhiannon morris 2023-08-27 19:05:25 +0200
• 3e3bf1b67f factor out this case !mode of {..} stuff rhiannon morris 2023-08-27 18:59:16 +0200
• 387d44431a add misc.coherence rhiannon morris 2023-08-27 18:34:19 +0200
• 2340b14407 partly improve coercions over constant lines rhiannon morris 2023-08-27 18:28:05 +0200
• edfe30ff63 update compare0 for type-directed whnf rhiannon morris 2023-08-26 21:32:15 +0200
• ba77c45c64 always print the direction in coe/comp rhiannon morris 2023-08-26 21:19:40 +0200
• f3f74d581a fix Main rhiannon morris 2023-08-26 21:07:10 +0200
• 22db2724ce make coercion computation type-directed like it should be rhiannon morris 2023-08-26 21:00:19 +0200
• 0bcb8c24db make an optional Loc non-optional rhiannon morris 2023-08-26 20:59:39 +0200
• a221380d61 more effect stuff, incl. ST rhiannon morris 2023-08-25 18:09:06 +0200
• 4b6b3853a1 make uses of eff more consistent rhiannon morris 2023-08-24 19:55:57 +0200
• 8264a1bb81 split up whnf module rhiannon morris 2023-08-24 18:42:26 +0200
• a24ebe0702 tycasePi etc don't actually need a scope of (S d) rhiannon morris 2023-08-24 17:45:37 +0200
• 688204f1a4 make some things private rhiannon morris 2023-08-24 17:45:20 +0200
• 09e39d6224 add some comments rhiannon morris 2023-08-24 17:45:12 +0200
• 7a6c4c61d1 wip 𝕎 rhiannon morris 2023-08-13 20:55:14 +0200
• 0dd3c231e6 fix a typo rhiannon morris 2023-08-13 13:45:29 +0200
• c5403a970e tweaks in bool.quox rhiannon morris 2023-08-12 10:28:19 +0200
• 5c4053e9d2 add some needed ωs for w-types rhiannon morris 2023-08-09 11:46:14 +0200
• 7cf3fa8bae add w types to parser rhiannon morris 2023-08-08 12:48:27 +0200
• 3cebc7b9b2 add W to parser syntax rhiannon morris 2023-08-08 06:39:52 +0200
• ca1adcce47 remove some noLocs rhiannon morris 2023-08-06 11:07:17 +0200
• 1da902d13a add W to internal language rhiannon morris 2023-08-06 10:46:55 +0200
• 00d92d3f25 add missing parens in pretty printer rhiannon morris 2023-08-12 10:24:59 +0200
• c6006682ca add CREDITS.md rhiannon morris 2023-08-10 16:44:28 +0200
• cf9bfc2159 example stuff rhiannon morris 2023-07-22 21:26:20 +0200
• f6b8a12fab some more example stuff rhiannon morris 2023-07-21 17:57:47 +0200
• 932469a91e make quantities optional and default to 1 rhiannon morris 2023-07-18 23:12:04 +0200
• 349cf2f477 remove unused Tighten impl rhiannon morris 2023-07-17 18:10:13 +0200
• 3c0989dcb2 maybe.quox rhiannon morris 2023-07-17 03:52:12 +0200