Lean4

Structures and record updates

Model named fields and construct precise modified copies.

11 minIntermediate
0/7 completed in this course
Lean workspaceWrite only the proof steps. The theorem above is fixed.
Enter after constructor adds both goal bullets
Exercise.leanLean 4.30.0
Sign in to check
Loading editor…

No problems detected so far. Run a check to hear from Lean.

ReadyLn 1, Col 1Pre-check passedLean 4