mathematics_in_lean_source icon indicating copy to clipboard operation
mathematics_in_lean_source copied to clipboard
Published 4 months ago • verified publisher icon avigad

Duplicated example in S03_Using_Theorems_and_Lemmas.lean

Open leepike opened this issue 2 months ago • 0 comments

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.

The example at https://github.com/leanprover-community/mathematics_in_lean/blob/2bf0e10dd0c02438b65110f85cd9b68a9dbe6e39/MIL/C02_Basics/S03_Using_Theorems_and_Lemmas.lean#L105

is duplicated at https://github.com/leanprover-community/mathematics_in_lean/blob/2bf0e10dd0c02438b65110f85cd9b68a9dbe6e39/MIL/C02_Basics/S03_Using_Theorems_and_Lemmas.lean#L116.

They are not duplicated in the solutions file.

leepike avatar Sep 26 '25 14:09 leepike