Commit Graph

Select branches

Hide Pull Requests

main

Mono Color

• 449b6762a6 codegen for functions. Steve Dunham 2024-08-08 22:59:07 -07:00
• 13dd77345c Process pattern in correct order Steve Dunham 2024-08-07 21:49:35 -07:00
• 9c5bdf5983 switch to fc Steve Dunham 2024-08-07 16:35:27 -07:00
• f5b1998afb checkpoint before FC Steve Dunham 2024-08-05 21:25:10 -07:00
• 09227e444a case checking partially working Steve Dunham 2024-08-04 15:46:43 -07:00
• 067a83960d checkpoint before case Steve Dunham 2024-08-02 21:39:39 -07:00
• 0bb2d48d72 Additional work Steve Dunham 2024-07-21 21:16:47 -07:00
• dc51e8af17 pre-binding Steve Dunham 2024-07-20 11:04:00 -07:00
• ac0cf8c3e8 mostly parsing tweaks Steve Dunham 2024-07-20 10:53:44 -07:00
• f0d0743ccb improved printing Steve Dunham 2024-07-17 22:13:11 -07:00
• 5bc9b4a9d9 notes Steve Dunham 2024-07-17 21:10:37 -07:00
• 3d477be52b Add more stuff to equality and more logging Steve Dunham 2024-07-16 22:07:37 -07:00
• c0f9262c9a nf the types, block comments, more eq example now that we have implicits Steve Dunham 2024-07-16 08:10:43 -07:00
• a385d1225d wip compile, drop let Steve Dunham 2024-07-14 16:48:11 -07:00
• 127a1e7f00 Remove unneeded implicities Steve Dunham 2024-07-14 16:04:26 -07:00
• 76fae34bcf unification seems to work for kovacs examples Steve Dunham 2024-07-13 09:32:49 -07:00
• b37fa56c70 fix issue in prettier Steve Dunham 2024-07-11 22:17:29 -07:00
• a4d851b563 implicits working, but _slow_ Steve Dunham 2024-07-09 22:43:24 -07:00
• edfa5ef443 fix issue with idris codegen Steve Dunham 2024-07-07 20:22:37 -04:00
• 6f638aac72 Initial work on metas Steve Dunham 2024-07-07 09:21:07 -04:00
• 46ddbc1f91 Preliminary work on data and holes Steve Dunham 2024-07-06 14:23:41 -04:00
• b9f921ab3b Add vscode extension, command line argument, and positioned error handling. Steve Dunham 2024-07-04 23:40:38 -04:00
• 0cad438f4d sugar on lambdas Steve Dunham 2024-06-25 13:57:41 -07:00
• d2fbd15b4a sugar on binders Steve Dunham 2024-06-25 13:53:15 -07:00
• 968327cdb3 working. checkpoint before messing with parser Steve Dunham 2024-06-25 13:27:11 -07:00
• a9c72d5a6d drop HOAS, add Monad stack. Steve Dunham 2024-04-11 19:57:02 -07:00
• 6a59aa97f8 Add monad, quote/eval broken Steve Dunham 2024-04-11 16:27:51 -07:00
• 46f9caccab checkpoint Steve Dunham 2024-04-11 15:21:13 -07:00
• 3b1bd4aad1 Fix implicit/explicit printing, various other issues Steve Dunham 2024-04-10 22:02:33 -07:00
• 203159d1da drop indexes Steve Dunham 2024-03-02 21:31:12 -08:00
• fc6801590f checkpoint before removing index Steve Dunham 2024-02-28 20:58:32 -08:00
• 349115d055 Checkpoint some stuff so I can rollback the rest. Steve Dunham 2023-09-30 06:40:54 -07:00
• 1f2afb279e Add prettyprint, merge plicity types Steve Dunham 2023-09-30 06:36:19 -07:00
• dec0fb6348 remove an index from Tm Steve Dunham 2023-08-11 21:11:15 -07:00
• f221f09423 more work on well scoped Steve Dunham 2023-07-18 22:28:08 -07:00
• 59f726ab96 Lib/TT.idr is well scoped Steve Dunham 2023-07-13 20:06:03 -07:00
• ed3ee96df9 parser good enough to elab kovacs stuff Steve Dunham 2023-05-20 22:54:01 -07:00
• 6850725d3b checkpoint Steve Dunham 2023-05-20 17:10:58 -07:00
• ec3cf04db4 fix comment parsing Steve Dunham 2023-05-20 16:20:36 -07:00
• 255e21f08a Checkpoint what I'd previously been working on. Steve Dunham 2023-05-19 21:10:57 -07:00
• 0358f224ae preliminary parser for data Steve Dunham 2023-04-10 21:48:36 -07:00
• 60dc4c4f08 add examples Steve Dunham 2023-04-10 21:35:01 -07:00
• c9fdd33770 Move unused files to ATTIC (not committed) Steve Dunham 2023-04-10 21:34:43 -07:00
• 5c294850a8 Checkpoint some existing changes. Steve Dunham 2023-04-10 21:24:07 -07:00
• 6e7a7c7d04 Parse modules Steve Dunham 2022-09-15 22:03:20 -07:00
• 1ed884eff9 Show instances, fixed a bunch of bugs in parsing Steve Dunham 2022-09-10 22:10:35 -07:00
• 39deff1465 chkpt Steve Dunham 2022-09-08 22:45:07 -07:00