fromLRAT — Mathlib

Lean4
/-- Main entry point. Given strings `cnf` and `lrat` with unparsed file data, and a name `name`,
adds `theorem name : type := proof` where `type` is a propositional theorem like
`∀ (a a_1 : Prop), (¬a ∧ ¬a_1 ∨ a ∧ ¬a_1) ∨ ¬a ∧ a_1 ∨ a ∧ a_1`.

Also creates auxiliaries named `name.ctx_1` (for the CNF formula)
and `name.proof_1` (for the LRAT proof), with `name` itself containing the reification proof. -/
def fromLRAT (cnf lrat : String) (name : Name) : MetaM Unit := do
  let (nvars, ctx, ctx', proof) ← fromLRATAux cnf lrat name
  let (type, value) := buildReify ctx ctx' proof nvars
  addDecl <| Declaration.thmDecl { name, levelParams := [], type, value }
Похожие утверждения