Update EnvExtensions.lean

pull/132/head
Pietro Monticone 1 year ago
parent f0f998298f
commit 2951747d1a

@ -67,7 +67,7 @@ structure InventoryTemplate where
/-- Depends on the type:
* Tactic: the tactic's name
* Lemma: fully qualified lemma name
* Definition: no restrictions (preferrably the definions fully qualified name)
* Definition: no restrictions (preferably the definitions fully qualified name)
-/
name: Name
/-- Only for Lemmas. To sort them into tabs -/

Loading…
Cancel
Save