Lean4

Binary trees

Every tree has positive size.

11 minIntermediate
0/5 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