@[reducible, inline]

abbrev Auto.LamCstrD.Nat.modEq (n a b : Nat) : Prop

Equations

• Auto.LamCstrD.Nat.modEq n a b = (a % n = b % n)

@[reducible, inline]

abbrev Auto.LamCstrD.Nat.ge (x y : Nat) : Prop

Equations

• Auto.LamCstrD.Nat.ge x y = y.le x

@[reducible, inline]

abbrev Auto.LamCstrD.Nat.gt (x y : Nat) : Prop

Equations

• Auto.LamCstrD.Nat.gt x y = y.lt x

@[reducible, inline]

abbrev Auto.LamCstrD.Nat.max (x y : Nat) : Nat

Equations

• Auto.LamCstrD.Nat.max x y = max x y

@[reducible, inline]

abbrev Auto.LamCstrD.Nat.min (x y : Nat) : Nat

Equations

• Auto.LamCstrD.Nat.min x y = min x y

@[reducible, inline]

abbrev Auto.LamCstrD.Int.modEq (n a b : Int) : Prop

Equations

• Auto.LamCstrD.Int.modEq n a b = (a % n = b % n)

@[reducible, inline]

abbrev Auto.LamCstrD.Int.ge (a b : Int) : Prop

Equations

• Auto.LamCstrD.Int.ge a b = b.le a

@[reducible, inline]

abbrev Auto.LamCstrD.Int.gt (a b : Int) : Prop

Equations

• Auto.LamCstrD.Int.gt a b = b.lt a

@[reducible, inline]

abbrev Auto.LamCstrD.Int.max (x y : Int) : Int

Equations

• Auto.LamCstrD.Int.max x y = max x y

@[reducible, inline]

abbrev Auto.LamCstrD.Int.min (x y : Int) : Int

Equations

• Auto.LamCstrD.Int.min x y = min x y

@[reducible, inline]

abbrev Auto.LamCstrD.String.ge (a b : String) : Prop

Equations

• Auto.LamCstrD.String.ge a b = (b = a ∨ b < a)

@[reducible, inline]

abbrev Auto.LamCstrD.String.gt (a b : String) : Prop

Equations

• Auto.LamCstrD.String.gt a b = (b < a)

@[reducible, inline]

abbrev Auto.LamCstrD.BitVec.uge {n : Nat} (a b : BitVec n) : Bool

Equations

• Auto.LamCstrD.BitVec.uge a b = b.ule a

@[reducible, inline]

abbrev Auto.LamCstrD.BitVec.ugt {n : Nat} (a b : BitVec n) : Bool

Equations

• Auto.LamCstrD.BitVec.ugt a b = b.ult a

@[reducible, inline]

abbrev Auto.LamCstrD.BitVec.sge {n : Nat} (a b : BitVec n) : Bool

Equations

• Auto.LamCstrD.BitVec.sge a b = b.sle a

@[reducible, inline]

abbrev Auto.LamCstrD.BitVec.sgt {n : Nat} (a b : BitVec n) : Bool

Equations

• Auto.LamCstrD.BitVec.sgt a b = b.slt a

@[reducible, inline]

abbrev Auto.LamCstrD.BitVec.propule {n : Nat} (a b : BitVec n) : Prop

Equations

• Auto.LamCstrD.BitVec.propule a b = (a.toFin ≤ b.toFin)

@[reducible, inline]

abbrev Auto.LamCstrD.BitVec.propult {n : Nat} (a b : BitVec n) : Prop

Equations

• Auto.LamCstrD.BitVec.propult a b = (a.toFin < b.toFin)

@[reducible, inline]

abbrev Auto.LamCstrD.BitVec.propsle {n : Nat} (a b : BitVec n) : Prop

Equations

• Auto.LamCstrD.BitVec.propsle a b = (a.toInt ≤ b.toInt)

@[reducible, inline]

abbrev Auto.LamCstrD.BitVec.propslt {n : Nat} (a b : BitVec n) : Prop

Equations

• Auto.LamCstrD.BitVec.propslt a b = (a.toInt < b.toInt)

@[reducible, inline]

abbrev Auto.LamCstrD.BitVec.propuge {n : Nat} (a b : BitVec n) : Prop

Equations

• Auto.LamCstrD.BitVec.propuge a b = Auto.LamCstrD.BitVec.propule b a

@[reducible, inline]

abbrev Auto.LamCstrD.BitVec.propugt {n : Nat} (a b : BitVec n) : Prop

Equations

• Auto.LamCstrD.BitVec.propugt a b = Auto.LamCstrD.BitVec.propult b a

@[reducible, inline]

abbrev Auto.LamCstrD.BitVec.propsge {n : Nat} (a b : BitVec n) : Prop

Equations

• Auto.LamCstrD.BitVec.propsge a b = Auto.LamCstrD.BitVec.propsle b a

@[reducible, inline]

abbrev Auto.LamCstrD.BitVec.propsgt {n : Nat} (a b : BitVec n) : Prop

Equations

• Auto.LamCstrD.BitVec.propsgt a b = Auto.LamCstrD.BitVec.propslt b a

@[reducible, inline]

abbrev Auto.LamCstrD.BitVec.smtHshiftLeft {n m : Nat} (a : BitVec n) (b : BitVec m) : BitVec n

Equations

• Auto.LamCstrD.BitVec.smtHshiftLeft a b = a.shiftLeft b.toNat

@[reducible, inline]

abbrev Auto.LamCstrD.BitVec.smtHushiftRight {n m : Nat} (a : BitVec n) (b : BitVec m) : BitVec n

Equations

• Auto.LamCstrD.BitVec.smtHushiftRight a b = a.ushiftRight b.toNat

@[reducible, inline]

abbrev Auto.LamCstrD.BitVec.smtHsshiftRight {n m : Nat} (a : BitVec n) (b : BitVec m) : BitVec n

Equations

• Auto.LamCstrD.BitVec.smtHsshiftRight a b = a.sshiftRight b.toNat

def Auto.LamExportUtils.exportError.ImpPolyLog : String

Equations

• Auto.LamExportUtils.exportError.ImpPolyLog = "Import versions of polymorphic logical " ++ "constants should have been eliminated"

def Auto.LamExportUtils.collectLamSortAtoms : Embedding.Lam.LamSort → Std.HashSet Nat

Equations

• Auto.LamExportUtils.collectLamSortAtoms (Auto.Embedding.Lam.LamSort.atom n) = Std.HashSet.emptyWithCapacity.insert n
• Auto.LamExportUtils.collectLamSortAtoms (Auto.Embedding.Lam.LamSort.base a) = Std.HashSet.emptyWithCapacity
• Auto.LamExportUtils.collectLamSortAtoms (a.func b) = (Auto.LamExportUtils.collectLamSortAtoms a).insertMany (Auto.LamExportUtils.collectLamSortAtoms b)

def Auto.LamExportUtils.collectLamSortsAtoms (ss : Array Embedding.Lam.LamSort) : Std.HashSet Nat

Equations

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

def Auto.LamExportUtils.collectLamSortBitVecLengths : Embedding.Lam.LamSort → Std.HashSet Nat

Equations

• Auto.LamExportUtils.collectLamSortBitVecLengths (Auto.Embedding.Lam.LamSort.base (Auto.Embedding.Lam.LamBaseSort.bv n)) = Std.HashSet.emptyWithCapacity.insert n
• Auto.LamExportUtils.collectLamSortBitVecLengths (a.func b) = (Auto.LamExportUtils.collectLamSortBitVecLengths a).insertMany (Auto.LamExportUtils.collectLamSortBitVecLengths b)
• Auto.LamExportUtils.collectLamSortBitVecLengths x✝ = Std.HashSet.emptyWithCapacity

def Auto.LamExportUtils.collectLamSortsBitVecLengths (ss : Array Embedding.Lam.LamSort) : Std.HashSet Nat

Equations

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

def Auto.LamExportUtils.collectLamBaseTermAtoms (b : Embedding.Lam.LamBaseTerm) : Lean.CoreM (Std.HashSet Nat)

Collect type atoms in a LamBaseTerm

Equations

• One or more equations did not get rendered due to their size.
• Auto.LamExportUtils.collectLamBaseTermAtoms b = do let s? ← pure none match s? with | some s => pure (Auto.LamExportUtils.collectLamSortAtoms s) | x => pure Std.HashSet.emptyWithCapacity

def Auto.LamExportUtils.collectLamTermAtoms (lamVarTy lamEVarTy : Array Embedding.Lam.LamSort) : Embedding.Lam.LamTerm → Lean.CoreM (Std.HashSet Nat × Std.HashSet Nat × Std.HashSet Nat)

The first hashset is the type atoms The second hashset is the term atoms The third hashset is the term etoms This function is called when we're trying to export terms from λ to external provers, e.g. Lean/Duper Therefore, we expect that eqI, forallEI, existEI and ``ite'does not occur in theLamTerm`

Equations

• One or more equations did not get rendered due to their size.
• Auto.LamExportUtils.collectLamTermAtoms lamVarTy lamEVarTy (Auto.Embedding.Lam.LamTerm.bvar a) = pure (Std.HashSet.emptyWithCapacity, Std.HashSet.emptyWithCapacity, Std.HashSet.emptyWithCapacity)

def Auto.LamExportUtils.collectLamTermsAtoms (lamVarTy lamEVarTy : Array Embedding.Lam.LamSort) (ts : Array Embedding.Lam.LamTerm) : Lean.CoreM (Std.HashSet Nat × Std.HashSet Nat × Std.HashSet Nat)

Equations

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

def Auto.LamExportUtils.collectLamTermNatConsts : Embedding.Lam.LamTerm → Std.HashSet Embedding.Lam.NatConst

Equations

• One or more equations did not get rendered due to their size.
• Auto.LamExportUtils.collectLamTermNatConsts (Auto.Embedding.Lam.LamTerm.base (Auto.Embedding.Lam.LamBaseTerm.ncst nc)) = Std.HashSet.emptyWithCapacity.insert nc
• Auto.LamExportUtils.collectLamTermNatConsts (Auto.Embedding.Lam.LamTerm.lam a body) = Auto.LamExportUtils.collectLamTermNatConsts body
• Auto.LamExportUtils.collectLamTermNatConsts x✝ = Std.HashSet.emptyWithCapacity

def Auto.LamExportUtils.collectLamTermsNatConsts (ts : Array Embedding.Lam.LamTerm) : Std.HashSet Embedding.Lam.NatConst

Equations

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

def Auto.LamExportUtils.collectLamTermIntConsts : Embedding.Lam.LamTerm → Std.HashSet Embedding.Lam.IntConst

Equations

• One or more equations did not get rendered due to their size.
• Auto.LamExportUtils.collectLamTermIntConsts (Auto.Embedding.Lam.LamTerm.base (Auto.Embedding.Lam.LamBaseTerm.icst ic)) = Std.HashSet.emptyWithCapacity.insert ic
• Auto.LamExportUtils.collectLamTermIntConsts (Auto.Embedding.Lam.LamTerm.lam a body) = Auto.LamExportUtils.collectLamTermIntConsts body
• Auto.LamExportUtils.collectLamTermIntConsts x✝ = Std.HashSet.emptyWithCapacity

def Auto.LamExportUtils.collectLamTermsIntConsts (ts : Array Embedding.Lam.LamTerm) : Std.HashSet Embedding.Lam.IntConst

Equations

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

def Auto.LamExportUtils.collectLamTermStringConsts : Embedding.Lam.LamTerm → Std.HashSet Embedding.Lam.StringConst

Equations

• One or more equations did not get rendered due to their size.
• Auto.LamExportUtils.collectLamTermStringConsts (Auto.Embedding.Lam.LamTerm.base (Auto.Embedding.Lam.LamBaseTerm.scst sc)) = Std.HashSet.emptyWithCapacity.insert sc
• Auto.LamExportUtils.collectLamTermStringConsts (Auto.Embedding.Lam.LamTerm.lam a body) = Auto.LamExportUtils.collectLamTermStringConsts body
• Auto.LamExportUtils.collectLamTermStringConsts x✝ = Std.HashSet.emptyWithCapacity

def Auto.LamExportUtils.collectLamTermsStringConsts (ts : Array Embedding.Lam.LamTerm) : Std.HashSet Embedding.Lam.StringConst

Equations

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

def Auto.LamExportUtils.collectLamTermBitvecs : Embedding.Lam.LamTerm → Std.HashSet Embedding.Lam.BitVecConst

Equations

• One or more equations did not get rendered due to their size.
• Auto.LamExportUtils.collectLamTermBitvecs (Auto.Embedding.Lam.LamTerm.base (Auto.Embedding.Lam.LamBaseTerm.bvcst bvc)) = Std.HashSet.emptyWithCapacity.insert bvc
• Auto.LamExportUtils.collectLamTermBitvecs (Auto.Embedding.Lam.LamTerm.lam a body) = Auto.LamExportUtils.collectLamTermBitvecs body
• Auto.LamExportUtils.collectLamTermBitvecs x✝ = Std.HashSet.emptyWithCapacity

def Auto.LamExportUtils.collectLamTermsBitvecs (ts : Array Embedding.Lam.LamTerm) : Std.HashSet Embedding.Lam.BitVecConst

Equations

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

def Auto.LamExportUtils.collectLamTermIteSorts : Embedding.Lam.LamTerm → Std.HashSet Embedding.Lam.LamSort

Equations

• One or more equations did not get rendered due to their size.
• Auto.LamExportUtils.collectLamTermIteSorts (Auto.Embedding.Lam.LamTerm.base (Auto.Embedding.Lam.LamBaseTerm.ite s)) = Std.HashSet.emptyWithCapacity.insert s
• Auto.LamExportUtils.collectLamTermIteSorts (Auto.Embedding.Lam.LamTerm.lam a body) = Auto.LamExportUtils.collectLamTermIteSorts body
• Auto.LamExportUtils.collectLamTermIteSorts x✝ = Std.HashSet.emptyWithCapacity

def Auto.LamExportUtils.collectLamTermsIteSorts (ts : Array Embedding.Lam.LamTerm) : Std.HashSet Embedding.Lam.LamSort

Equations

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

def Auto.Lam2D.interpLamBaseSortAsUnlifted : Embedding.Lam.LamBaseSort → Lean.Expr

Equations

• Auto.Lam2D.interpLamBaseSortAsUnlifted Auto.Embedding.Lam.LamBaseSort.prop = Lean.Expr.sort Lean.Level.zero
• Auto.Lam2D.interpLamBaseSortAsUnlifted Auto.Embedding.Lam.LamBaseSort.bool = Lean.Expr.const `Bool []
• Auto.Lam2D.interpLamBaseSortAsUnlifted Auto.Embedding.Lam.LamBaseSort.nat = Lean.Expr.const `Nat []
• Auto.Lam2D.interpLamBaseSortAsUnlifted Auto.Embedding.Lam.LamBaseSort.int = Lean.Expr.const `Int []
• Auto.Lam2D.interpLamBaseSortAsUnlifted (Auto.Embedding.Lam.LamBaseSort.isto0 Auto.Pos.xH) = Lean.Expr.const `String []
• Auto.Lam2D.interpLamBaseSortAsUnlifted (Auto.Embedding.Lam.LamBaseSort.isto0 Auto.Pos.xH.xO) = Lean.Expr.const `Empty []
• Auto.Lam2D.interpLamBaseSortAsUnlifted (Auto.Embedding.Lam.LamBaseSort.isto0 p) = Lean.Expr.const `Empty []
• Auto.Lam2D.interpLamBaseSortAsUnlifted (Auto.Embedding.Lam.LamBaseSort.bv n) = (Lean.Expr.const `BitVec []).app (Lean.Expr.lit (Lean.Literal.natVal n))

def Auto.Lam2D.interpPropConstAsUnlifted : Embedding.Lam.PropConst → Lean.CoreM Lean.Expr

Equations

• One or more equations did not get rendered due to their size.
• Auto.Lam2D.interpPropConstAsUnlifted Auto.Embedding.Lam.PropConst.trueE = pure (Lean.Expr.const `True [])
• Auto.Lam2D.interpPropConstAsUnlifted Auto.Embedding.Lam.PropConst.falseE = pure (Lean.Expr.const `False [])
• Auto.Lam2D.interpPropConstAsUnlifted Auto.Embedding.Lam.PropConst.not = pure (Lean.Expr.const `Not [])
• Auto.Lam2D.interpPropConstAsUnlifted Auto.Embedding.Lam.PropConst.and = pure (Lean.Expr.const `And [])
• Auto.Lam2D.interpPropConstAsUnlifted Auto.Embedding.Lam.PropConst.or = pure (Lean.Expr.const `Or [])
• Auto.Lam2D.interpPropConstAsUnlifted Auto.Embedding.Lam.PropConst.iff = pure (Lean.Expr.const `Iff [])

def Auto.Lam2D.interpBoolConstAsUnlifted : Embedding.Lam.BoolConst → Lean.CoreM Lean.Expr

Equations

• Auto.Lam2D.interpBoolConstAsUnlifted Auto.Embedding.Lam.BoolConst.ofProp = pure (Lean.Expr.const `Auto.Bool.ofProp [])
• Auto.Lam2D.interpBoolConstAsUnlifted Auto.Embedding.Lam.BoolConst.trueb = pure (Lean.Expr.const `Bool.true [])
• Auto.Lam2D.interpBoolConstAsUnlifted Auto.Embedding.Lam.BoolConst.falseb = pure (Lean.Expr.const `Bool.false [])
• Auto.Lam2D.interpBoolConstAsUnlifted Auto.Embedding.Lam.BoolConst.notb = pure (Lean.Expr.const `Bool.not [])
• Auto.Lam2D.interpBoolConstAsUnlifted Auto.Embedding.Lam.BoolConst.andb = pure (Lean.Expr.const `Bool.and [])
• Auto.Lam2D.interpBoolConstAsUnlifted Auto.Embedding.Lam.BoolConst.orb = pure (Lean.Expr.const `Bool.or [])

def Auto.Lam2D.interpNatConstAsUnlifted : Embedding.Lam.NatConst → Lean.CoreM Lean.Expr

Equations

• Auto.Lam2D.interpNatConstAsUnlifted (Auto.Embedding.Lam.NatConst.natVal n) = pure (Lean.Expr.lit (Lean.Literal.natVal n))
• Auto.Lam2D.interpNatConstAsUnlifted Auto.Embedding.Lam.NatConst.nadd = pure (Lean.Expr.const `Nat.add [])
• Auto.Lam2D.interpNatConstAsUnlifted Auto.Embedding.Lam.NatConst.nsub = pure (Lean.Expr.const `Nat.sub [])
• Auto.Lam2D.interpNatConstAsUnlifted Auto.Embedding.Lam.NatConst.nmul = pure (Lean.Expr.const `Nat.mul [])
• Auto.Lam2D.interpNatConstAsUnlifted Auto.Embedding.Lam.NatConst.ndiv = pure (Lean.Expr.const `Nat.div [])
• Auto.Lam2D.interpNatConstAsUnlifted Auto.Embedding.Lam.NatConst.nmod = pure (Lean.Expr.const `Nat.mod [])
• Auto.Lam2D.interpNatConstAsUnlifted Auto.Embedding.Lam.NatConst.nle = pure (Lean.Expr.const `Nat.le [])
• Auto.Lam2D.interpNatConstAsUnlifted Auto.Embedding.Lam.NatConst.nlt = pure (Lean.Expr.const `Nat.lt [])
• Auto.Lam2D.interpNatConstAsUnlifted Auto.Embedding.Lam.NatConst.nmax = pure (Lean.Expr.const `Nat.max [])
• Auto.Lam2D.interpNatConstAsUnlifted Auto.Embedding.Lam.NatConst.nmin = pure (Lean.Expr.const `Nat.min [])

def Auto.Lam2D.interpIntConstAsUnlifted : Embedding.Lam.IntConst → Lean.CoreM Lean.Expr

Equations

• Auto.Lam2D.interpIntConstAsUnlifted Auto.Embedding.Lam.IntConst.iofNat = pure (Lean.Expr.const `Int.ofNat [])
• Auto.Lam2D.interpIntConstAsUnlifted Auto.Embedding.Lam.IntConst.inegSucc = pure (Lean.Expr.const `Int.negSucc [])
• Auto.Lam2D.interpIntConstAsUnlifted Auto.Embedding.Lam.IntConst.ineg = pure (Lean.Expr.const `Int.neg [])
• Auto.Lam2D.interpIntConstAsUnlifted Auto.Embedding.Lam.IntConst.iabs = pure (Lean.Expr.const `Auto.Int.abs [])
• Auto.Lam2D.interpIntConstAsUnlifted Auto.Embedding.Lam.IntConst.iadd = pure (Lean.Expr.const `Int.add [])
• Auto.Lam2D.interpIntConstAsUnlifted Auto.Embedding.Lam.IntConst.isub = pure (Lean.Expr.const `Int.sub [])
• Auto.Lam2D.interpIntConstAsUnlifted Auto.Embedding.Lam.IntConst.imul = pure (Lean.Expr.const `Int.mul [])
• Auto.Lam2D.interpIntConstAsUnlifted Auto.Embedding.Lam.IntConst.idiv = pure (Lean.Expr.const `Int.tdiv [])
• Auto.Lam2D.interpIntConstAsUnlifted Auto.Embedding.Lam.IntConst.imod = pure (Lean.Expr.const `Int.tmod [])
• Auto.Lam2D.interpIntConstAsUnlifted Auto.Embedding.Lam.IntConst.iediv = pure (Lean.Expr.const `Int.ediv [])
• Auto.Lam2D.interpIntConstAsUnlifted Auto.Embedding.Lam.IntConst.iemod = pure (Lean.Expr.const `Int.emod [])
• Auto.Lam2D.interpIntConstAsUnlifted Auto.Embedding.Lam.IntConst.ile = pure (Lean.Expr.const `Int.le [])
• Auto.Lam2D.interpIntConstAsUnlifted Auto.Embedding.Lam.IntConst.ilt = pure (Lean.Expr.const `Int.lt [])
• Auto.Lam2D.interpIntConstAsUnlifted Auto.Embedding.Lam.IntConst.imax = pure (Lean.Expr.const `Auto.LamCstrD.Int.max [])
• Auto.Lam2D.interpIntConstAsUnlifted Auto.Embedding.Lam.IntConst.imin = pure (Lean.Expr.const `Auto.LamCstrD.Int.min [])

def Auto.Lam2D.interpStringConstAsUnlifted : Embedding.Lam.StringConst → Lean.CoreM Lean.Expr

Equations

• Auto.Lam2D.interpStringConstAsUnlifted (Auto.Embedding.Lam.StringConst.strVal s) = pure (Lean.Expr.lit (Lean.Literal.strVal s))
• Auto.Lam2D.interpStringConstAsUnlifted Auto.Embedding.Lam.StringConst.slength = pure (Lean.Expr.const `String.length [])
• Auto.Lam2D.interpStringConstAsUnlifted Auto.Embedding.Lam.StringConst.sapp = pure (Lean.Expr.const `String.append [])
• Auto.Lam2D.interpStringConstAsUnlifted Auto.Embedding.Lam.StringConst.sle = pure (Lean.Expr.const `Auto.String.le [])
• Auto.Lam2D.interpStringConstAsUnlifted Auto.Embedding.Lam.StringConst.slt = pure (Lean.Expr.const `Auto.String.lt [])
• Auto.Lam2D.interpStringConstAsUnlifted Auto.Embedding.Lam.StringConst.sprefixof = pure (Lean.Expr.const `String.isPrefixOf [])
• Auto.Lam2D.interpStringConstAsUnlifted Auto.Embedding.Lam.StringConst.srepall = pure (Lean.Expr.const `String.replace [])

def Auto.Lam2D.interpBitVecConstAsUnlifted : Embedding.Lam.BitVecConst → Lean.CoreM Lean.Expr

Equations

• One or more equations did not get rendered due to their size.
• Auto.Lam2D.interpBitVecConstAsUnlifted (Auto.Embedding.Lam.BitVecConst.bvofNat n) = pure ((Lean.Expr.const `BitVec.ofNat []).app (Lean.Expr.lit (Lean.Literal.natVal n)))
• Auto.Lam2D.interpBitVecConstAsUnlifted (Auto.Embedding.Lam.BitVecConst.bvtoNat n) = pure ((Lean.Expr.const `BitVec.toNat []).app (Lean.Expr.lit (Lean.Literal.natVal n)))
• Auto.Lam2D.interpBitVecConstAsUnlifted (Auto.Embedding.Lam.BitVecConst.bvofInt n) = pure ((Lean.Expr.const `BitVec.ofInt []).app (Lean.Expr.lit (Lean.Literal.natVal n)))
• Auto.Lam2D.interpBitVecConstAsUnlifted (Auto.Embedding.Lam.BitVecConst.bvtoInt n) = pure ((Lean.Expr.const `BitVec.toInt []).app (Lean.Expr.lit (Lean.Literal.natVal n)))
• Auto.Lam2D.interpBitVecConstAsUnlifted (Auto.Embedding.Lam.BitVecConst.bvmsb n) = pure ((Lean.Expr.const `BitVec.msb []).app (Lean.Expr.lit (Lean.Literal.natVal n)))
• Auto.Lam2D.interpBitVecConstAsUnlifted (Auto.Embedding.Lam.BitVecConst.bvaOp n Auto.Embedding.Lam.BVAOp.add) = pure ((Lean.Expr.const `BitVec.add []).app (Lean.Expr.lit (Lean.Literal.natVal n)))
• Auto.Lam2D.interpBitVecConstAsUnlifted (Auto.Embedding.Lam.BitVecConst.bvaOp n Auto.Embedding.Lam.BVAOp.sub) = pure ((Lean.Expr.const `BitVec.sub []).app (Lean.Expr.lit (Lean.Literal.natVal n)))
• Auto.Lam2D.interpBitVecConstAsUnlifted (Auto.Embedding.Lam.BitVecConst.bvaOp n Auto.Embedding.Lam.BVAOp.mul) = pure ((Lean.Expr.const `BitVec.mul []).app (Lean.Expr.lit (Lean.Literal.natVal n)))
• Auto.Lam2D.interpBitVecConstAsUnlifted (Auto.Embedding.Lam.BitVecConst.bvaOp n Auto.Embedding.Lam.BVAOp.urem) = pure ((Lean.Expr.const `BitVec.umod []).app (Lean.Expr.lit (Lean.Literal.natVal n)))
• Auto.Lam2D.interpBitVecConstAsUnlifted (Auto.Embedding.Lam.BitVecConst.bvaOp n Auto.Embedding.Lam.BVAOp.srem) = pure ((Lean.Expr.const `BitVec.srem []).app (Lean.Expr.lit (Lean.Literal.natVal n)))
• Auto.Lam2D.interpBitVecConstAsUnlifted (Auto.Embedding.Lam.BitVecConst.bvaOp n Auto.Embedding.Lam.BVAOp.smod) = pure ((Lean.Expr.const `BitVec.smod []).app (Lean.Expr.lit (Lean.Literal.natVal n)))
• Auto.Lam2D.interpBitVecConstAsUnlifted (Auto.Embedding.Lam.BitVecConst.bvneg n) = pure ((Lean.Expr.const `BitVec.neg []).app (Lean.Expr.lit (Lean.Literal.natVal n)))
• Auto.Lam2D.interpBitVecConstAsUnlifted (Auto.Embedding.Lam.BitVecConst.bvabs n) = pure ((Lean.Expr.const `BitVec.abs []).app (Lean.Expr.lit (Lean.Literal.natVal n)))
• Auto.Lam2D.interpBitVecConstAsUnlifted (Auto.Embedding.Lam.BitVecConst.bvand n) = pure ((Lean.Expr.const `BitVec.and []).app (Lean.Expr.lit (Lean.Literal.natVal n)))
• Auto.Lam2D.interpBitVecConstAsUnlifted (Auto.Embedding.Lam.BitVecConst.bvor n) = pure ((Lean.Expr.const `BitVec.or []).app (Lean.Expr.lit (Lean.Literal.natVal n)))
• Auto.Lam2D.interpBitVecConstAsUnlifted (Auto.Embedding.Lam.BitVecConst.bvxor n) = pure ((Lean.Expr.const `BitVec.xor []).app (Lean.Expr.lit (Lean.Literal.natVal n)))
• Auto.Lam2D.interpBitVecConstAsUnlifted (Auto.Embedding.Lam.BitVecConst.bvnot n) = pure ((Lean.Expr.const `BitVec.not []).app (Lean.Expr.lit (Lean.Literal.natVal n)))

def Auto.Lam2D.interpLamSortAsUnlifted (tyVal : Std.HashMap Nat Lean.Expr) : Embedding.Lam.LamSort → Lean.CoreM Lean.Expr

Takes a s : LamSort and produces the un-lifted version of s.interp (note that s.interp is lifted)

Equations

• One or more equations did not get rendered due to their size.
• Auto.Lam2D.interpLamSortAsUnlifted tyVal (Auto.Embedding.Lam.LamSort.base a) = pure (Auto.Lam2D.interpLamBaseSortAsUnlifted a)

def Auto.Lam2D.interpOtherConstAsUnlifted (tyVal : Std.HashMap Nat Lean.Expr) (oc : Embedding.Lam.OtherConst) : Lean.MetaM Lean.Expr

Equations

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

def Auto.Lam2D.interpLamBaseTermAsUnlifted (tyVal : Std.HashMap Nat Lean.Expr) : Embedding.Lam.LamBaseTerm → Lean.MetaM Lean.Expr

Equations

• One or more equations did not get rendered due to their size.
• Auto.Lam2D.interpLamBaseTermAsUnlifted tyVal (Auto.Embedding.Lam.LamBaseTerm.pcst pc) = liftM (Auto.Lam2D.interpPropConstAsUnlifted pc)
• Auto.Lam2D.interpLamBaseTermAsUnlifted tyVal (Auto.Embedding.Lam.LamBaseTerm.bcst bc) = liftM (Auto.Lam2D.interpBoolConstAsUnlifted bc)
• Auto.Lam2D.interpLamBaseTermAsUnlifted tyVal (Auto.Embedding.Lam.LamBaseTerm.ncst nc) = liftM (Auto.Lam2D.interpNatConstAsUnlifted nc)
• Auto.Lam2D.interpLamBaseTermAsUnlifted tyVal (Auto.Embedding.Lam.LamBaseTerm.icst ic) = liftM (Auto.Lam2D.interpIntConstAsUnlifted ic)
• Auto.Lam2D.interpLamBaseTermAsUnlifted tyVal (Auto.Embedding.Lam.LamBaseTerm.scst sc) = liftM (Auto.Lam2D.interpStringConstAsUnlifted sc)
• Auto.Lam2D.interpLamBaseTermAsUnlifted tyVal (Auto.Embedding.Lam.LamBaseTerm.bvcst bvc) = liftM (Auto.Lam2D.interpBitVecConstAsUnlifted bvc)
• Auto.Lam2D.interpLamBaseTermAsUnlifted tyVal (Auto.Embedding.Lam.LamBaseTerm.ocst oc) = Auto.Lam2D.interpOtherConstAsUnlifted tyVal oc

def Auto.Lam2D.interpLamTermAsUnlifted (tyVal varVal etomVal : Std.HashMap Nat Lean.Expr) (lctx : Nat) : Embedding.Lam.LamTerm → Lean.MetaM Lean.Expr

Takes a t : LamTerm and produces the un-lifted version of t.interp. lctx is for pretty printing

Note that etoms generated by the verified checker do not directly correspond to Lean expressions. Therefore, we need to introduce new free variables to represent etoms.

Equations

• One or more equations did not get rendered due to their size.
• Auto.Lam2D.interpLamTermAsUnlifted tyVal varVal etomVal lctx (Auto.Embedding.Lam.LamTerm.base b) = Auto.Lam2D.interpLamBaseTermAsUnlifted tyVal b
• Auto.Lam2D.interpLamTermAsUnlifted tyVal varVal etomVal lctx (Auto.Embedding.Lam.LamTerm.bvar a) = pure (Lean.Expr.bvar a)

def Auto.Lam2D.natConstSimpNFList : List (Lean.Name × Lean.Expr)

Equations

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

def Auto.Lam2D.intConstSimpNFList : List (Lean.Name × Lean.Expr)

Equations

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

def Auto.Lam2D.stringConstSimpNFList : List (Lean.Name × Lean.Expr)

Equations

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

def Auto.Lam2D.bitVecConstSimpNFList : List (Lean.Name × Lean.Expr)

Equations

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

def Auto.Lam2D.lamBaseTermSimpNFList : List (Lean.Name × Lean.Expr)

Equations

• Auto.Lam2D.lamBaseTermSimpNFList = Auto.Lam2D.natConstSimpNFList ++ Auto.Lam2D.intConstSimpNFList ++ Auto.Lam2D.stringConstSimpNFList ++ Auto.Lam2D.bitVecConstSimpNFList

def Auto.Lam2D.lamBaseTermSimpNFMap : Std.HashMap Lean.Name Lean.Expr

Equations

• Auto.Lam2D.lamBaseTermSimpNFMap = Std.HashMap.ofList Auto.Lam2D.lamBaseTermSimpNFList

def Auto.Lam2D.approxSimpNF (e : Lean.Expr) : Lean.CoreM Lean.Expr

Equations

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