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

refactor: Lint

Browse source
This commit is contained in:
jstoobysmith 2024-09-16 10:14:25 -04:00
parent 6713e2f86d
commit c0ac40440d
1 changed files with 5 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

5
HepLean/Meta/Informal.lean
View file

@ -51,6 +51,7 @@ declare_syntax_cat informalAssignment
/-- The syntax describing an informal assignment of `ident` to a string. -/
syntax (name := informalAssignment) ident ":≈" str : informalAssignment
/-- The syntax describing an informal assignment of `ident` to a list. -/
syntax (name := informalAssignmentDeps) ident ":≈" "[" sepBy(term, ",") "]" : informalAssignment
/-- The syntax for the command informal_definition. -/
@ -131,18 +132,22 @@ def $name : InformalLemma := {
dependencies := $(dep_def?.getD (← `([])))
})
/-- Is true if and only if a `ConstantInfo` corresponds to an `InformalLemma` or a
`InformalDefinition`. -/
def isInformal (c : ConstantInfo) : Bool :=
match c with
| ConstantInfo.defnInfo c =>
if c.type.isAppOf ``InformalDefinition ∨ c.type.isAppOf ``InformalLemma then true else false
| _ => false
/-- Is true if and only if a `ConstantInfo` corresponds to an `InformalLemma`. -/
def isInformalLemma (c : ConstantInfo) : Bool :=
match c with
| ConstantInfo.defnInfo c =>
if c.type.isAppOf ``InformalLemma then true else false
| _ => false
/-- Is true if and only if a `ConstantInfo` corresponds to an `InformalDefinition`. -/
def isInformalDef (c : ConstantInfo) : Bool :=
match c with
| ConstantInfo.defnInfo c =>