Def hi

Modification history

2022-11-22 21:55

test/DocCommands.lean

chore: remove upstreamed tactics 11-21 (#684)

Deleted hi View on Github →

2022-10-24 03:11

test/DocCommands.lean

feat: port `copy_doc_string` command (#494)

Added hi View on Github →