DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

doc: Note about expected dependencies

Browse source
This commit is contained in:
jstoobysmith 2024-09-15 10:49:54 -04:00
parent b1cfbe9a7a
commit b24908c51e
1 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
HepLean/Meta/Informal.lean
View file

@ -15,6 +15,8 @@ open Lean Elab System
/-! TODO: Can likely make this a bona-fide command. -/
/-! TODO: Add expected dependencies. -/
/-- The structure representating an informal definition. -/
structure InformalDefinition where
/-- The name of the informal definition. This is autogenerated. -/