opaque auto.native : Lean.Option Bool

@[implemented_by _private.Auto.Solver.Native.0.Auto.Solver.Native.queryNativeUnsafe]

opaque Auto.Solver.Native.queryNative : Array Lemma → Array Lemma → Lean.MetaM Lean.Expr

def Auto.Solver.Native.emulateNative (lemmas : Array Lemma) : Array Lemma → Lean.MetaM Lean.Expr

Emulate a native prover. When given lemmas h₁, ⋯, hₙ, the prover returns sorryAx (h₁ → ⋯ → hₙ → ⊥) Bool.false h₁ ⋯ hₙ Inhabitation lemmas are ignored

Equations

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