Documentation Verification Report

FromLRAT

📁 Source: Mathlib/Tactic/Sat/FromLRAT.lean

Statistics

Metric	Count
Definitions `Clause`, `expr`, `lits`, `proof`, `LClause`, `depth`, `expr`, `lits`, `LRATStep`, `parseDimacs`, `parseInt`, `parseInts`, `parseLRAT`, `parseNat`, `parseNats`, `buildClause`, `buildClauses`, `buildConj`, `buildProof`, `buildProofStep`, `buildReify`, `mkPS`, `reifyClause`, `reifyClause1`, `reifyFmla`, `reifyLiteral`, `reifyVar`, `v`, `commandLrat_proof_Example____`, `fromLRAT`, `fromLRATAux`, `termFrom_lrat___`, `Clause`, `cons`, `nil`, `reify`, `Fmla`, `and`, `one`, `proof`, `reify`, `subsumes`, `Literal`, `negate`, `ofInt`, `reify`, `implies`, `mk`, `neg`, `satisfies`, `satisfies_fmla`, `instToExprLiteral`	52
Theorems `prop`, `reify_and`, `reify_one`, `reify_zero`, `proof_of_subsumes`, `refute`, `prop`, `reify_one`, `reify_or`, `prop`, `subsumes_left`, `subsumes_right`, `subsumes_self`, `prop`, `reify_neg`, `reify_pos`, `by_cases`, `mk_implies`, `prop`	19
Total	71

Mathlib.Tactic.Sat

Definitions

Name	Category	Theorems
`Clause` 📖	CompData	—
`LClause` 📖	CompData	—
`LRATStep` 📖	CompData	—
`buildClause` 📖	CompOp	—
`buildClauses` 📖	CompOp	—
`buildConj` 📖	CompOp	—
`buildProof` 📖	CompOp	—
`buildProofStep` 📖	CompOp	—
`buildReify` 📖	CompOp	—
`commandLrat_proof_Example____` 📖	CompOp	—
`fromLRAT` 📖	CompOp	—
`fromLRATAux` 📖	CompOp	—
`termFrom_lrat___` 📖	CompOp	—

Mathlib.Tactic.Sat.Clause

Definitions

Name	Category	Theorems
`expr` 📖	CompOp	—
`lits` 📖	CompOp	—
`proof` 📖	CompOp	—

Mathlib.Tactic.Sat.LClause

Definitions

Name	Category	Theorems
`depth` 📖	CompOp	—
`expr` 📖	CompOp	—
`lits` 📖	CompOp	—

Mathlib.Tactic.Sat.Parser

Definitions

Name	Category	Theorems
`parseDimacs` 📖	CompOp	—
`parseInt` 📖	CompOp	—
`parseInts` 📖	CompOp	—
`parseLRAT` 📖	CompOp	—
`parseNat` 📖	CompOp	—
`parseNats` 📖	CompOp	—

Mathlib.Tactic.Sat.buildReify

Definitions

Name	Category	Theorems
`mkPS` 📖	CompOp	—
`reifyClause` 📖	CompOp	—
`reifyClause1` 📖	CompOp	—
`reifyFmla` 📖	CompOp	—
`reifyLiteral` 📖	CompOp	—
`reifyVar` 📖	CompOp	—
`v` 📖	CompOp	—

Sat

Definitions

Name	Category	Theorems
`Clause` 📖	CompOp	—
`Fmla` 📖	CompOp	—
`Literal` 📖	CompData	—
`instToExprLiteral` 📖	CompOp	—

Sat.Clause

Definitions

Name	Category	Theorems
`cons` 📖	CompOp	2 math math: `reify_one`, `reify_and`
`nil` 📖	CompOp	2 math math: `reify_zero`, `reify_one`
`reify` 📖	CompData	2 math math: `reify_zero`, `reify_one`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`reify_and` 📖	mathematical	`Sat.Literal.reify` `reify`	`cons`	—	`Sat.Literal.reify.prop` `by_contra` `reify.prop`
`reify_one` 📖	mathematical	`Sat.Literal.reify`	`reify` `cons` `nil`	—	`reify.prop` `reify_and` `reify_zero`
`reify_zero` 📖	mathematical	—	`reify` `nil`	—	—

Sat.Clause.reify

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prop` 📖	—	`Sat.Clause.reify` `Sat.Valuation.satisfies`	—	—	—

Sat.Fmla

Definitions

Name	Category	Theorems
`and` 📖	CompOp	1 math math: `reify_or`
`one` 📖	CompOp	1 math math: `reify_one`
`proof` 📖	MathDef	1 math math: `proof_of_subsumes`
`reify` 📖	CompData	1 math math: `reify_one`
`subsumes` 📖	CompData	1 math math: `subsumes_self`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`proof_of_subsumes` 📖	mathematical	`subsumes` `one`	`proof`	—	`Sat.Valuation.satisfies_fmla.prop` `subsumes.prop`
`refute` 📖	—	`proof` `Sat.Literal` `Sat.Valuation.implies` `reify`	—	—	`reify.prop` `Sat.Valuation.mk_implies`
`reify_one` 📖	mathematical	`Sat.Clause.reify`	`reify` `one`	—	`Sat.Clause.reify.prop`
`reify_or` 📖	mathematical	`reify`	`and`	—	`by_contra` `reify.prop` `Sat.Valuation.satisfies_fmla.prop`
`subsumes_left` 📖	—	`subsumes` `and`	—	—	`subsumes.prop`
`subsumes_right` 📖	—	`subsumes` `and`	—	—	`subsumes.prop`
`subsumes_self` 📖	mathematical	—	`subsumes`	—	—

Sat.Fmla.reify

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prop` 📖	—	`Sat.Fmla.reify` `Sat.Valuation.satisfies_fmla`	—	—	—

Sat.Fmla.subsumes

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prop` 📖	—	`Sat.Fmla.subsumes` `Sat.Clause` `Sat.Fmla`	—	—	—

Sat.Literal

Definitions

Name	Category	Theorems
`negate` 📖	CompOp	—
`ofInt` 📖	CompOp	—
`reify` 📖	CompData	2 math math: `reify_pos`, `reify_neg`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`reify_neg` 📖	mathematical	—	`reify` `neg`	—	—
`reify_pos` 📖	mathematical	—	`reify` `pos`	—	—

Sat.Literal.reify

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prop` 📖	—	`Sat.Literal.reify` `Sat.Valuation.neg`	—	—	—

Sat.Valuation

Definitions

Name	Category	Theorems
`implies` 📖	MathDef	—
`mk` 📖	CompOp	—
`neg` 📖	MathDef	—
`satisfies` 📖	MathDef	1 math math: `satisfies_fmla.prop`
`satisfies_fmla` 📖	CompData	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`by_cases` 📖	—	—	—	—	—
`mk_implies` 📖	—	`implies`	—	—	`zero_add`

Sat.Valuation.satisfies_fmla

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prop` 📖	mathematical	`Sat.Valuation.satisfies_fmla` `Sat.Clause` `Sat.Fmla`	`Sat.Valuation.satisfies`	—	—

---

← Back to Index