Def command.quot

Modification history

2022-11-15 08:49

Mathlib/Tactic/CommandQuote.lean

chore: remove obsolete CommandQuote (#602)

Deleted command.quot View on Github →

2022-10-20 15:23

Mathlib/Tactic/CommandQuote.lean

chore: update lean + std4 10-20 (#483)

Modified command.quot View on Github →

2022-07-01 15:19

Mathlib/Tactic/CommandQuote.lean

fix: make `(command|...) produce correct type (#297) …

Added command.quot View on Github →