Documentation

Lean.Elab.Tactic.BVDecide.Frontend.BVDecide.Reflect

This module contains the implementation of the reflection monad, used by all other components of this directory.

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

A BitVec atom.

  • width : Nat

    The width of the BitVec that is being abstracted.

  • atomNumber : Nat

    A unique numeric identifier for the atom.

  • synthetic : Bool

    Whether the atom is synthetic. The effect of this is that values for this atom are not considered for the counter example deriviation. This is for example useful when we introduce an atom over an expression, together with additional lemmas that fully describe the behavior of the atom.

The state of the reflection monad

@[reducible, inline]

The reflection monad, used to track BitVec variables that we see as we traverse the context.

Equations

A reified version of an Expr representing a BVExpr.

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

A reified version of an Expr representing a BVPred.

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

A reified version of an Expr representing a BVLogicalExpr.

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

A reified version of an Expr representing a BVLogicalExpr that we know to be true.

Run a reflection computation as a MetaM one.

Equations

Retrieve the atoms as pairs of their width and expression.

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

Retrieve a BitVec.Assignment representing the atoms we found so far.

Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
def Lean.Elab.Tactic.BVDecide.Frontend.M.lookup (e : Expr) (width : Nat) (synthetic : Bool) :

Look up an expression in the atoms, recording it if it has not previously appeared.

Equations
  • One or more equations did not get rendered due to their size.
@[specialize #[]]
def Lean.Elab.Tactic.BVDecide.Frontend.M.simplifyBinaryProof' (mkFRefl : ExprExpr) (fst : Expr) (fproof : Option Expr) (mkSRefl : ExprExpr) (snd : Expr) (sproof : Option Expr) :
Equations
@[specialize #[]]
def Lean.Elab.Tactic.BVDecide.Frontend.M.simplifyBinaryProof (mkRefl : ExprExpr) (fst : Expr) (fproof : Option Expr) (snd : Expr) (sproof : Option Expr) :
Equations
@[specialize #[]]
def Lean.Elab.Tactic.BVDecide.Frontend.M.simplifyTernaryProof (mkRefl : ExprExpr) (fst : Expr) (fproof : Option Expr) (snd : Expr) (sproof : Option Expr) (thd : Expr) (tproof : Option Expr) :
Equations

The state of the lemma reflection monad.

@[reducible, inline]

The lemma reflection monad. It extends the usual reflection monad M by adding the ability to add additional top level lemmas on the fly.

Equations
Equations

Add another top level lemma.

Equations
  • One or more equations did not get rendered due to their size.
@[specialize #[]]
Equations
  • One or more equations did not get rendered due to their size.
@[specialize #[]]
Equations
  • One or more equations did not get rendered due to their size.
@[specialize #[]]
Equations
  • One or more equations did not get rendered due to their size.