Skip to content

Commit 472efb9

Browse files
eric-wieserb-mehta
authored andcommitted
chore: add argument names to the Tree constructor (leanprover-community#39587)
1 parent a83e92a commit 472efb9

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

Mathlib/Data/Tree/Basic.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,7 @@ additional data. We provide the notation `a △ b` for making a `Tree Unit` with
3030
/-- A binary tree with values stored in non-leaf nodes. -/
3131
inductive Tree.{u} (α : Type u) : Type u
3232
| nil : Tree α
33-
| node : αTree αTree α Tree α
33+
| node (value : α) (left : Tree α) (right : Tree α) : Tree α
3434
deriving DecidableEq, Repr
3535
compile_inductive% Tree
3636

0 commit comments

Comments
 (0)