9 lines
239 B
Text
9 lines
239 B
Text
class Pretty (α : Type u) where
|
||
pretty : α → Std.Format
|
||
|
||
export Pretty (pretty)
|
||
|
||
def concat (xs : List ((α : Type u) × Pretty α × α)) : Std.Format :=
|
||
match xs with
|
||
| [] => ""
|
||
| ⟨_, _, v⟩ :: xs => pretty v ++ concat xs
|