Commits at 3b014ccc29cb9e879991a89523e9da0007eb1312
3b014ccc
Type checker is almost done hopefully
Anthony Wang
authored at
2026-05-05 00:20:51 -0400
Anthony Wang
comitted at
2026-05-05 00:20:51 -0400
a99cea45
Add support for variable names
Anthony Wang
authored at
2026-05-04 17:39:50 -0400
Anthony Wang
comitted at
2026-05-04 17:39:50 -0400
5165d725
toString for new type checker
Anthony Wang
authored at
2026-05-03 22:54:48 -0400
Anthony Wang
comitted at
2026-05-03 22:54:48 -0400
9e5da10a
Better notation
Anthony Wang
authored at
2026-05-03 22:28:58 -0400
Anthony Wang
comitted at
2026-05-03 22:28:58 -0400
23dd54fb
demo
Rey Li
authored at
2026-05-03 20:37:00 -0400
Rey Li
comitted at
2026-05-03 20:37:00 -0400
0cb4fc63
Commit more bad code
Anthony Wang
authored at
2026-05-03 03:27:19 -0400
Anthony Wang
comitted at
2026-05-03 03:27:19 -0400
3ff64e64
Cursed dependent type stuff
Anthony Wang
authored at
2026-05-03 00:24:21 -0400
Anthony Wang
comitted at
2026-05-03 00:24:21 -0400
631afd86
Fix bug in Lurk port as well
Anthony Wang
authored at
2026-05-01 14:57:33 -0400
Anthony Wang
comitted at
2026-05-01 14:57:33 -0400
2150026d
Prove that uLean type checker is as consistent as Lean
Dan Klishch
authored at
2026-05-01 14:08:49 -0400
Dan Klishch
comitted at
2026-05-01 14:08:49 -0400
e7a247de
Lean type checker bug fix
Dan Klishch
authored at
2026-05-01 14:08:09 -0400
Dan Klishch
comitted at
2026-05-01 14:08:09 -0400
b699a330
Move Lurk files to root dir, try with a larger proof, delete old garbage
Anthony Wang
authored at
2026-04-29 14:14:45 -0400
Anthony Wang
comitted at
2026-04-29 14:14:45 -0400
c5d06832
More slightly nontrivial proofs
Anthony Wang
authored at
2026-04-29 13:58:00 -0400
Anthony Wang
comitted at
2026-04-29 13:58:00 -0400
e0867123
Small tweaks to Lean impl of μLean
Anthony Wang
authored at
2026-04-29 10:19:23 -0400
Anthony Wang
comitted at
2026-04-29 10:19:23 -0400
3bb5cccf
successful (inelegant) protocol implementation
Rey Li
authored at
2026-04-29 00:30:32 -0400
Rey Li
comitted at
2026-04-29 00:30:32 -0400
bcb71a24
set up factoring example for better running
Rey Li
authored at
2026-04-26 13:55:56 -0400
Rey Li
comitted at
2026-04-26 13:55:56 -0400
b4984fc0
factoring test proof made
Rey Li
authored at
2026-04-26 13:48:21 -0400
Rey Li
comitted at
2026-04-26 13:48:21 -0400
a8be2654
significant partial working progress towards creating a hiding protocol
Rey Li
authored at
2026-04-26 13:11:59 -0400
Rey Li
comitted at
2026-04-26 13:11:59 -0400
6716245a
Fix stupid typo (thanks Claude)
Anthony Wang
authored at
2026-04-24 14:45:14 -0400
Anthony Wang
comitted at
2026-04-24 14:45:14 -0400
183ddaad
de Bruijn indices (Lurk version is still broken)
Anthony Wang
authored at
2026-04-24 14:39:43 -0400
Anthony Wang
comitted at
2026-04-24 14:39:43 -0400
e84b5aa9
Name it μLean
Anthony Wang
authored at
2026-04-24 14:27:40 -0400
Anthony Wang
comitted at
2026-04-24 14:27:40 -0400
ec83994f
Use field elements instead of strings for variable names
Anthony Wang
authored at
2026-04-24 14:08:21 -0400
Anthony Wang
comitted at
2026-04-24 14:08:21 -0400
80ffed3a
Swap Term and Typ to match the usual convention
Anthony Wang
authored at
2026-04-22 17:01:14 -0400
Anthony Wang
comitted at
2026-04-22 17:01:14 -0400
e18f6136
Use finite field elements instead of strings for better perf
Actually I have no idea if this actually improves perf or not...
Anthony Wang
authored at
2026-04-22 12:23:34 -0400
Anthony Wang
comitted at
2026-04-22 12:25:19 -0400
1aef3614
Bump Lean version
Anthony Wang
authored at
2026-04-20 16:00:41 -0400
Anthony Wang
comitted at
2026-04-20 16:00:41 -0400
09248633
Add Lurk dir patch
Anthony Wang
authored at
2026-04-20 13:52:03 -0400
Anthony Wang
comitted at
2026-04-20 13:52:03 -0400
7e531a32
Broken protocol code
Anthony Wang
authored at
2026-04-20 11:29:41 -0400
Anthony Wang
comitted at
2026-04-20 11:29:41 -0400
7731f06c
Passing all test cases now
Anthony Wang
authored at
2026-04-18 20:20:11 -0400
Anthony Wang
comitted at
2026-04-18 20:20:11 -0400
786a1c9e
Type checker in Lurk finally works!!!
Anthony Wang
authored at
2026-04-18 17:40:08 -0400
Anthony Wang
comitted at
2026-04-18 17:40:20 -0400
26daa600
Lurk port almost somewhat works now I guess
Anthony Wang
authored at
2026-04-08 14:35:40 -0400
Anthony Wang
comitted at
2026-04-08 14:35:40 -0400
041cf99d
Implement natural numbers
Anthony Wang
authored at
2026-04-05 22:56:41 -0400
Anthony Wang
comitted at
2026-04-05 22:56:41 -0400
Commits for
3b014ccc29cb9e879991a89523e9da0007eb1312
Viewing range
3b014ccc
~ 041cf99d