William Ball

wball pushed to main at wball/perga

2024-12-05 19:05:49 -08:00

7e3a347485 applied fix to other ascriptions

wball pushed to main at wball/perga

2024-12-05 18:57:30 -08:00

c0e0c37689 more peano, fixed bug in checking ascriptions of definitions

wball pushed to main at wball/tree-sitter-perga

2024-12-02 20:40:55 -08:00

bed94f3d41 impredicative/predicative split

973acd4151 new type hierarchy

Compare 2 commits »

wball pushed to main at wball/perga

2024-12-02 20:40:22 -08:00

84e44b0e33 made universe hierarchy predicative except for lowest

wball pushed to main at wball/perga

2024-12-01 21:43:31 -08:00

5eb68fe360 more optional ascriptions (surprisingly large change)

wball pushed to main at wball/tree-sitter-perga

2024-12-01 21:39:10 -08:00

c3fbf3368f accommodated new ascriptions

wball pushed to main at wball/perga.nvim

2024-12-01 20:56:02 -08:00

b53ddc01fd oops, fixed highlighting on axioms

wball pushed to main at wball/tree-sitter-perga

2024-12-01 20:54:23 -08:00

6de6e3d801 new syntax, also block comments are totally broken

wball pushed to main at wball/perga.nvim

2024-12-01 20:53:50 -08:00

36f6058413 updates

wball pushed to main at wball/perga

2024-12-01 18:17:29 -08:00

959f425afa updated README with changes

05ae14b5e7 made repl preserve environment

0a57180cb1 updated examples to new syntax

9f5c308131 IR success!

cdafab0d94 compiles, getting stuck somewhere though

Compare 8 commits »

wball pushed to main at wball/perga

2024-11-30 19:01:22 -08:00

57bffe00b5 updated readme

wball pushed to main at wball/perga

2024-11-30 00:11:10 -08:00

9e54c14c65 fixed .cabal expecting README.md

wball pushed to main at wball/perga

2024-11-29 20:42:46 -08:00

0c004688c7 made preprocessor not reinclude files multiple times

wball pushed to main at wball/perga

2024-11-29 18:19:58 -08:00

f8a684a173 updated README a bit to talk more about (im)predicativity, abandoned markdown

wball pushed to main at wball/perga

2024-11-28 14:32:49 -08:00

58168e461d clear binders after each definition (!!!)

wball pushed to main at wball/perga

2024-11-28 13:39:47 -08:00

9afa90d3af added universes; documentation and examples forthcoming

wball pushed to main at wball/perga

2024-11-28 10:49:00 -08:00

652467f02c fixed but in let impl, work on proving recursion

wball pushed to main at wball/perga.nvim

2024-11-23 10:43:13 -08:00

2645b608e8 updated to support let

wball pushed to main at wball/tree-sitter-perga

2024-11-23 10:39:42 -08:00

6e1878db5d support functions in let

wball deleted branch let from wball/perga

2024-11-23 10:37:17 -08:00