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

• d61101f786 nix cleanup rhiannon morris 2022-05-04 18:35:43 +0200
• f5f2c4399e move lib to subdir rhiannon morris 2022-05-04 17:44:38 +0200
• 7f415328a2 wip nix rhiannon morris 2022-05-04 17:09:49 +0200
• 4973ce15bd add some keywords rhiannon morris 2022-05-04 15:30:52 +0200
• 96e81584b6 isCons → NonEmpty rhiannon morris 2022-05-04 15:30:37 +0200
• 2d7110b9c6 tokens in separate file rhiannon morris 2022-05-04 15:30:08 +0200
• 38ecabdda8 numbers with bases rhiannon morris 2022-05-04 03:11:37 +0200
• e13cd50175 pokes in TAP rhiannon morris 2022-05-04 00:49:18 +0200
• fa5beb4e2b decimal numbers rhiannon morris 2022-05-04 00:49:09 +0200
• 699c6a5ca1 token stuff rhiannon morris 2022-05-03 02:03:22 +0200
• a510737462 .gitignore rhiannon morris 2022-05-03 02:02:25 +0200
• ce3342f330 deriving rhiannon morris 2022-05-02 22:40:28 +0200
• ba3612d836 %default total rhiannon morris 2022-05-02 22:38:37 +0200
• 9ae0e36a65 time for sirdi rhiannon morris 2022-05-02 20:51:19 +0200
• f503cf5734 start some lexer stuff rhiannon morris 2022-05-02 17:13:13 +0200
• df3505a04c use vars in makefiles i guess rhiannon morris 2022-05-02 02:41:00 +0200
• 434f0e08d1 make skip functions make more sense rhiannon morris 2022-05-02 02:27:03 +0200
• e3384d4e6e support TAP 13 for /usr/bin/prove's benefit rhiannon morris 2022-05-02 00:19:09 +0200
• cf119694c1 move executable to subdir rhiannon morris 2022-05-01 17:11:13 +0200
• 874187f252 some bibs rhiannon morris 2022-04-30 14:35:00 +0200
• 9e76bcc765 check quantites of subject and global rhiannon morris 2022-04-27 22:57:56 +0200
• 468c3a4c6a grtt -> qtt rhiannon morris 2022-04-27 21:58:09 +0200
• 45825ebc17 makefiles. again rhiannon morris 2022-04-27 20:07:08 +0200
• 1eace0039e a few tests rhiannon morris 2022-04-27 20:06:39 +0200
• 6bffd6a11c add converse υ rule for elim rhiannon morris 2022-04-27 20:04:29 +0200
• 81e1f331e0 move main to ./Main.idr rhiannon morris 2022-04-27 20:04:03 +0200
• 66c96cb3c4 %inline, etc rhiannon morris 2022-04-27 15:07:32 +0200
• a690ca1277 return an exit code from TAP.run rhiannon morris 2022-04-27 15:04:10 +0200
• d062f79176 fix yaml doc indent rhiannon morris 2022-04-27 15:03:29 +0200
• d74b056e11 put single line yaml info on one line rhiannon morris 2022-04-27 14:57:41 +0200
• bcd4544692 Show Quox.Equal.Mode rhiannon morris 2022-04-27 14:56:39 +0200
• 7629404097 reexport Data.List.Elem from Quox.Error rhiannon morris 2022-04-27 14:55:19 +0200
• 64fe3a5a0f list all modules in quox.ipkg rhiannon morris 2022-04-27 14:54:22 +0200
• d28366c90b add TAP framework. if you could call it that rhiannon morris 2022-04-26 18:17:59 +0200
• f33e96e198 separate executable into its own package rhiannon morris 2022-04-25 18:10:59 +0200
• 4cbe88496c remove old broken makefile rhiannon morris 2022-04-24 17:20:08 +0200
• 5ea7880e38 typechecker stuff rhiannon morris 2022-04-24 00:21:30 +0200
• b433957eec ignore *~ rhiannon morris 2022-04-24 00:21:23 +0200
• 56ddd59fb4 make lteZero' and lteSucc' into hints rhiannon morris 2022-04-12 16:48:23 +0200
• de6ec78e23 add Tighten Term etc rhiannon morris 2022-04-12 13:31:46 +0200
• 67d8c59cd1 make tighten into an interface rhiannon morris 2022-04-11 23:36:01 +0200
• 7faca8ac27 use Subset instead of relevant product rhiannon morris 2022-04-11 23:34:28 +0200
• d912614d7d fiddling rhiannon morris 2022-04-11 23:34:18 +0200
• 25f4923fac merge duplicate Nat LTE' rhiannon morris 2022-04-11 23:33:32 +0200
• 2446655b08 move BannerOpts to PrettyOpts rhiannon morris 2022-04-11 21:58:33 +0200
• 9088ec02a0 make syntax cyan not blue rhiannon morris 2022-04-11 14:09:48 +0200
• 00997dff13 banner stuff rhiannon morris 2022-04-11 14:09:37 +0200
• 13b173322b %inline, etc rhiannon morris 2022-04-09 18:55:08 +0200
• 46b29b8e72 more ScopeTerm stuff rhiannon morris 2022-04-09 18:54:47 +0200
• 4722e144a3 add ScopeTerm rhiannon morris 2022-04-09 15:31:22 +0200
• 38260d3838 producing a proof in TC is not worth it rhiannon morris 2022-04-08 03:47:11 +0200
• ce9d55becc fix a warning rhiannon morris 2022-04-08 00:14:05 +0200
• e6d942ce1b add Dim.toConst rhiannon morris 2022-04-06 20:32:56 +0200
• 2c1ca7e19b improve equality somewhat rhiannon morris 2022-04-06 20:31:38 +0200
• 981f543509 agda fiddling rhiannon morris 2022-04-06 20:21:02 +0200
• 3ea12fef67 important feature: banner rhiannon morris 2022-03-07 01:19:26 +0100
• 8f860cc1be an agda file that is kinda like how datatypes would be encoded in quox origin/main rhiannon morris 2022-02-27 02:19:22 +0100
• f7571ce6c3 add makefile for deps rhiannon morris 2022-02-27 02:18:44 +0100
• 071704076e add start of Quox.Equal rhiannon morris 2022-02-27 02:18:16 +0100
• 362c9354cf add Var.tighten* rhiannon morris 2022-02-27 02:17:51 +0100
• ddba87262d add Injective instances, etc rhiannon morris 2022-02-27 02:17:42 +0100
• 6cb862033a add Quox.OPE rhiannon morris 2022-02-27 02:17:09 +0100
• 8248f8ed82 remove some implicits that can now be inferred rhiannon morris 2022-02-27 02:06:52 +0100
• 3722c769cf add some properties of Var.Compare rhiannon morris 2022-02-27 01:50:01 +0100
• c653fcb664 more formatting stuff rhiannon morris 2022-02-27 01:49:42 +0100
• e264a18e21 i found an issue about that 0 bug rhiannon morris 2022-02-27 01:48:37 +0100
• 7d821b20ef add %inline to some instances rhiannon morris 2022-02-27 01:47:55 +0100
• 76c02adf03 add Subst.one rhiannon morris 2022-02-27 01:46:44 +0100
• 3ea9db1c82 export bodies of CanShift instances and rename Compose to Map rhiannon morris 2022-02-27 01:46:31 +0100
• d8f869d6df some DimEqs properties rhiannon morris 2022-02-27 01:45:10 +0100
• 7ea494c3cd add some whnf stuff rhiannon morris 2022-02-27 01:44:20 +0100
• 9b260529c8 add casts to Integer for Var & Shift rhiannon morris 2022-02-27 01:36:08 +0100
• 610b5fde2d add DimEqs.get etc rhiannon morris 2022-02-27 01:33:52 +0100
• 8006ae4c40 add DimEqs.zeroEq rhiannon morris 2022-02-27 01:31:52 +0100
• d52d1c3181 add %inlines rhiannon morris 2022-02-27 01:30:23 +0100
• bc3230e000 rename Error.inj to one rhiannon morris 2022-02-27 01:28:49 +0100
• 9bd02d185a add Context.pure rhiannon morris 2022-02-27 01:28:36 +0100
• 762ef780af formatting etc rhiannon morris 2022-02-27 01:28:19 +0100
• 3efff3e96d rewrite Context.(!!) rhiannon morris 2022-02-27 01:22:02 +0100
• 88338050fc start of type stuff rhiannon morris 2021-12-23 19:05:50 +0100
• f363dc3122 add DimEq rhiannon morris 2021-12-23 19:05:00 +0100
• 730cedc4c0 wap quantities in pi to match grtt rhiannon morris 2021-12-23 19:03:37 +0100
• b5cfc7b23b add pushSubsts' to just have the term without proof rhiannon morris 2021-12-23 19:03:04 +0100
• 568dba6f0b CanShift Dim rhiannon morris 2021-12-23 19:01:39 +0100
• a11e4d5ef1 add LT/LTE for vars rhiannon morris 2021-12-23 19:01:24 +0100
• acfa1b96be bikeshedding again rhiannon morris 2021-12-23 16:05:55 +0100
• 1924250fcd add lengthPrf0 for contexts rhiannon morris 2021-12-23 16:03:49 +0100
• 7bc58625a1 add (?!) for nondependent contexts rhiannon morris 2021-12-23 15:56:01 +0100
• 2a5b8ec815 bikeshedding rhiannon morris 2021-12-23 15:55:18 +0100
• dbd0a3a451 add name to type arg in Context' and Telescope' rhiannon morris 2021-12-23 15:54:16 +0100
• c75332be44 remove old typecheck stuff rhiannon morris 2021-12-23 15:53:40 +0100
• e833322ebe add separate type for dimension endpoints rhiannon morris 2021-12-23 15:52:56 +0100
• 40fde92823 change printing of binders rhiannon morris 2021-12-23 15:50:19 +0100
• d5530f9884 remove Eval.idr which is no good rhiannon morris 2021-11-29 14:50:53 +0100
• fce293caa7 fix an outdated comment rhiannon morris 2021-11-21 14:59:41 +0100
• 37230a8032 tweak some type signatures rhiannon morris 2021-11-21 14:59:27 +0100
• 81fc802fa8 move SomeTerm stuff rhiannon morris 2021-09-26 11:11:30 +0200
• 65e45dcc79 use stdlib Elem and add note why not also stdlib OpenUnion rhiannon morris 2021-09-26 10:55:07 +0200
• 2b1a043280 beginnings of typechecker, maybe rhiannon morris 2021-09-25 20:24:23 +0200
• 11856fa96a eval stuff rhiannon morris 2021-09-25 20:24:04 +0200