Lee Pike

icon indicating a website link https://leepike.github.io/ icon indicating an email [email protected]

icon location Portland, Oregon, USA

Results 3 issues of Lee Pike

Document fixed bit-width assumptions in Copilot

@fredyr pointed out that queues are implemented using `Word16`, regardless of the user type and suggested we should document all the non-user specified fixed types used, particularly for porting programs...

Shrinking base types

Add a way to optionally shrink base types. One way to do this would be to define a "shrink-like" class, and the user can define instances for types they want...

enhancement

Duplicated example in S03_Using_Theorems_and_Lemmas.lean

I believe the Python scripts that generate the exercises / solutions has a bug causing a duplicate exercise to be generated in [https://github.com/leanprover-community/mathematics_in_lean/blob/master/MIL/C02_Basics/S03_Using_Theorems_and_Lemmas.lean](https://github.com/leanprover-community/mathematics_in_lean/blob/master/MIL/C02_Basics/S03_Using_Theorems_and_Lemmas.lean). The example at [https://github.com/leanprover-community/mathematics_in_lean/blob/2bf0e10dd0c02438b65110f85cd9b68a9dbe6e39/MIL/C02_Basics/S03_Using_Theorems_and_Lemmas.lean#L105](https://github.com/leanprover-community/mathematics_in_lean/blob/2bf0e10dd0c02438b65110f85cd9b68a9dbe6e39/MIL/C02_Basics/S03_Using_Theorems_and_Lemmas.lean#L105) is duplicated at...