Def Type.Hello

Modification history

2025-06-17 18:33
MathlibTest/CommandStart.lean
feat: a linter to enforce formatting (#24465) …
Added Type.HelloView on Github →