This module contains infrastructure for proofs by native evaluation (native decide, bv_decide). Such proofs involve a native computation using the Lean kernel, and then asserting the result of that computation as an axiom towards the logic.

inductive Lean.Meta.NativeEqTrueResult : Type

• success (prf : Expr) : NativeEqTrueResult

  The given expression e evalutes to true. prf is a proof of e = true.

• notTrue : NativeEqTrueResult

  The given expression e evalutes to false.

def Lean.Meta.nativeEqTrue (tacticName : Name) (e : Expr) (axiomDeclRange? : Option Syntax := none) : MetaM NativeEqTrueResult

A call to nativeEqTrue tacName e, where e is a closed value of type Bool, will compile and run that value, check that it evaluates to true, and if so, will add an axiom asserting e = true and return that axiom.

It is the basis for native_decide and bv_decide tactics.

Equations

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