def FirstOrder.Parser.Attr.syntax_simp_proc : Lean.ParserDescr

Simplification procedure

Equations

• One or more equations did not get rendered due to their size.

def FirstOrder.Parser.Attr.syntax_simp : Lean.ParserDescr

The simp_syntax attribute registers simp lemmas for FOL syntax.

Equations

• One or more equations did not get rendered due to their size.

def FirstOrder.tacticSyntax_simp__ : Lean.ParserDescr

syntax_simp is a non-terminal tactic to simplify FOL syntax. It is a macro of simp only [syntax_simp].

Equations

• One or more equations did not get rendered due to their size.