Mario Carneiro
Mario Carneiro
When playing OneSaber maps, this allows choosing to use the left or right hand based on the active controller used to select the "PLAY" or "RESTART GAME" button. The active...
You can't use the keyboard when not in VR currently. There is a debug setting `DEBUG_KEYBOARD` that allows you to click on the buttons manually it but this breaks it...
We should move all output to stderr (mostly error messages), except possibly timing info. This way, output-producing modes like `--export` can print their results on stdout without it getting confused...
Currently, unlike the rest of the program `verify` will fail fast upon discovering any error in the proof at all. This makes sense because for the most part errors are...
A parsing algorithm for $j comments is needed to get basic grammar data, in particular, the identification of syntax proofs by typecode.
Reported at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/syntax.20of.20inductive.20definitions .
- [x] Depends on: #735 - [x] Depends on: #737 - [x] Depends on: #738 This adds `RBSet.upperBound?` symmetric to `lowerBound?`, and lifts all the RBNode theorems to RBSet (and...
This adds an implementation of exact (IEEE conforming) rounding from `Rat` to `Float` rounding nearest ties to even. Note that unlike most other lean functions (but like most float functions),...
These lemmas are separate from the rest and need not be pulled in by the main file.