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 `lrat_proof` command is the name of the theorem to define,
and the statement (written in CNF format) and the proof (in LRAT format).
For example:
```
lrat_proof foo
"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 see the theorem statement by hovering over the word `foo`.
* You can use the `example` keyword in place of `foo` to avoid generating a theorem.
* You can use the `include_str` macro in place of the two strings
to load CNF / LRAT files from disk.
-/
@[command_parser 1000]
public meta def commandLrat_proof_Example____ : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.Sat.commandLrat_proof_Example____ 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "lrat_proof ")
(ParserDescr.binary✝ `orelse (ParserDescr.const✝ `ident)
(ParserDescr.nodeWithAntiquot✝ "example" `token.example (ParserDescr.symbol✝ "example"))))
(ParserDescr.unary✝ `group (ParserDescr.const✝ `ppSpace)))
(ParserDescr.cat✝ `term 1024))
(ParserDescr.unary✝ `group (ParserDescr.const✝ `ppSpace)))
(ParserDescr.cat✝ `term 1024))
