Lean4
/-- A macro for producing SAT proofs from CNF / LRAT files.
These files are commonly used in the SAT community for writing proofs.
The input to the `from_lrat` term syntax is two string expressions with
the statement (written in CNF format) and the proof (in LRAT format).
For example:
```
def foo := from_lrat
"p cnf 2 4 1 2 0 -1 2 0 1 -2 0 -1 -2 0"
"5 -2 0 4 3 0 5 d 3 4 0 6 1 0 5 1 0 6 d 1 0 7 0 5 2 6 0"
```
produces a theorem:
```
foo : ∀ (a a_1 : Prop), (¬a ∧ ¬a_1 ∨ a ∧ ¬a_1) ∨ ¬a ∧ a_1 ∨ a ∧ a_1
```
* You can use this term after `have :=` or in `def foo :=` to produce the term
without constraining the type.
* You can use it when a specific type is expected, but it currently does not
pay any attention to the shape of the goal and always produces the same theorem,
so you can only use this to do alpha renaming.
* You can use the `include_str` macro in place of the two strings
to load CNF / LRAT files from disk.
-/
@[term_parser 1000]
public meta def termFrom_lrat___ : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.Sat.termFrom_lrat___ 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "from_lrat ") (ParserDescr.cat✝ `term 1024))
(ParserDescr.unary✝ `group (ParserDescr.const✝ `ppSpace)))
(ParserDescr.cat✝ `term 1024))
