Leni Aniva aniva
  • Stanford University Centaur Group
  • https://leni.sh
  • Admin of this website

  • Joined on 2023-08-21
aniva opened issue aniva/Pantograph#6 2023-08-23 13:27:41 -07:00
The termination of Lean.Level serialization is not ensured
aniva pushed to io/serial at aniva/Pantograph 2023-08-23 13:25:42 -07:00
7160f8aa61 Merge branch 'dev' into io/serial
85440e0278 Unify json and unknown error into command error
Compare 2 commits »
aniva closed issue aniva/Pantograph#4 2023-08-23 13:22:30 -07:00
Redundant error messages
aniva closed issue aniva/Pantograph#3 2023-08-23 13:22:25 -07:00
Dead code in proof tree
aniva pushed to dev at aniva/Pantograph 2023-08-23 13:22:19 -07:00
85440e0278 Unify json and unknown error into command error
aniva deleted branch misc/cleanup from aniva/Pantograph 2023-08-23 13:22:19 -07:00
aniva merged pull request aniva/Pantograph#5 2023-08-23 13:22:18 -07:00
Remove dead code and consolidate error types
aniva created pull request aniva/Pantograph#5 2023-08-23 13:21:36 -07:00
Remove dead code and consolidate error types
aniva commented on issue aniva/Pantograph#4 2023-08-23 13:16:07 -07:00
Redundant error messages

This error category and json error have been consolidated into one command error, used to indicate an error that makes it impossible to proceed to any individual command function.

aniva pushed to misc/cleanup at aniva/Pantograph 2023-08-23 13:15:16 -07:00
85440e0278 Unify json and unknown error into command error
aniva created branch misc/cleanup in aniva/Pantograph 2023-08-23 13:15:16 -07:00
aniva pushed to io/serial at aniva/Pantograph 2023-08-23 12:51:26 -07:00
e63f7c9afa Add proper printing of sorts
aniva created pull request aniva/To-The-Stars#1 2023-08-22 23:22:45 -07:00
WIP: Up to chapter 10
aniva pushed to wiki at aniva/To-The-Stars 2023-08-22 23:21:12 -07:00
aniva created branch wiki in aniva/To-The-Stars 2023-08-22 23:21:12 -07:00
aniva created branch diagrams in aniva/To-The-Stars 2023-08-22 23:21:12 -07:00
aniva pushed to diagrams at aniva/To-The-Stars 2023-08-22 23:21:12 -07:00
aniva deleted branch notes from aniva/To-The-Stars 2023-08-22 23:21:03 -07:00
aniva created branch notes in aniva/To-The-Stars 2023-08-22 23:20:07 -07:00
aniva pushed to notes at aniva/To-The-Stars 2023-08-22 23:20:07 -07:00