Def Ordnode.repr

Modification history

2023-07-19 05:37

Mathlib/Data/Ordmap/Ordnode.lean

chore: cleanup whitespace (#5988) …

Modified Ordnode.repr View on Github →

2023-06-12 01:02

Mathlib/Data/Ordmap/Ordnode.lean

chore: formatting issues (#4947)

Modified Ordnode.repr View on Github →

2023-05-01 11:02

Mathlib/Data/Ordmap/Ordnode.lean

feat: port Mathlib.Data.Ordmap.Ordnode (#1455)

Added Ordnode.repr View on Github →