Interpreted sorts
- prop : LamBaseSort
- bool : LamBaseSort
- nat : LamBaseSort
- int : LamBaseSort
- isto0 : Pos → LamBaseSort
- bv (n : Nat) : LamBaseSort
Instances For
Equations
- Auto.Embedding.Lam.instToExprLamBaseSort = { toExpr := Auto.Embedding.Lam.toExprLamBaseSort✝, toTypeExpr := Lean.Expr.const `Auto.Embedding.Lam.LamBaseSort [] }
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Auto.Embedding.Lam.instReprLamBaseSort = { reprPrec := fun (s : Auto.Embedding.Lam.LamBaseSort) (n : Nat) => s.reprPrec n }
Equations
- Auto.Embedding.Lam.LamBaseSort.prop.toString = "Prop"
- Auto.Embedding.Lam.LamBaseSort.bool.toString = "Bool"
- Auto.Embedding.Lam.LamBaseSort.nat.toString = "Nat"
- Auto.Embedding.Lam.LamBaseSort.int.toString = "Int"
- (Auto.Embedding.Lam.LamBaseSort.isto0 Auto.Pos.xH).toString = "String"
- (Auto.Embedding.Lam.LamBaseSort.isto0 a).toString = "Empty"
- (Auto.Embedding.Lam.LamBaseSort.bv a).toString = toString "BitVec " ++ toString a ++ toString ""
Instances For
Equations
- Auto.Embedding.Lam.LamBaseSort.prop.beq Auto.Embedding.Lam.LamBaseSort.prop = true
- Auto.Embedding.Lam.LamBaseSort.bool.beq Auto.Embedding.Lam.LamBaseSort.bool = true
- Auto.Embedding.Lam.LamBaseSort.nat.beq Auto.Embedding.Lam.LamBaseSort.nat = true
- Auto.Embedding.Lam.LamBaseSort.int.beq Auto.Embedding.Lam.LamBaseSort.int = true
- (Auto.Embedding.Lam.LamBaseSort.isto0 p₁).beq (Auto.Embedding.Lam.LamBaseSort.isto0 p₂) = p₁.beq p₂
- (Auto.Embedding.Lam.LamBaseSort.bv n).beq (Auto.Embedding.Lam.LamBaseSort.bv m) = n.beq m
- x✝¹.beq x✝ = false
Instances For
Equations
Instances For
Equations
- Auto.Embedding.Lam.LamBaseSort.prop.interp = Auto.Embedding.GLift Prop
- Auto.Embedding.Lam.LamBaseSort.bool.interp = Auto.Embedding.GLift Bool
- Auto.Embedding.Lam.LamBaseSort.nat.interp = Auto.Embedding.GLift Nat
- Auto.Embedding.Lam.LamBaseSort.int.interp = Auto.Embedding.GLift Int
- (Auto.Embedding.Lam.LamBaseSort.isto0 a).interp = Auto.Embedding.Lam.LamBaseSort.isto0_interp a
- (Auto.Embedding.Lam.LamBaseSort.bv a).interp = Auto.Embedding.GLift (BitVec a)
Instances For
Instances For
Equations
Equations
Equations
- Auto.Embedding.Lam.instToExprLamSort = { toExpr := Auto.Embedding.Lam.toExprLamSort✝, toTypeExpr := Lean.Expr.const `Auto.Embedding.Lam.LamSort [] }
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Auto.Embedding.Lam.instReprLamSort = { reprPrec := fun (s : Auto.Embedding.Lam.LamSort) (n : Nat) => s.reprPrec n }
Equations
Instances For
Equations
Equations
- (Auto.Embedding.Lam.LamSort.atom m).beq (Auto.Embedding.Lam.LamSort.atom n) = m.beq n
- (Auto.Embedding.Lam.LamSort.base m).beq (Auto.Embedding.Lam.LamSort.base n) = m.beq n
- (m₁.func n₁).beq (m₂.func n₂) = (m₁.beq m₂ && n₁.beq n₂)
- x✝¹.beq x✝ = false
Instances For
Equations
Given a
and [ty₀, ty₁, ⋯, tyᵢ₋₁]
, return ty₀ → ty₁ → ⋯ → tyᵢ₋₁ → a
Equations
- a.mkFuncs tys = List.foldr (fun (s cur : Auto.Embedding.Lam.LamSort) => s.func cur) a tys
Instances For
Given a
and [ty₀, ty₁, ⋯, tyᵢ₋₁]
, return tyᵢ₋₁ → ⋯ → ty₁ → ty₀ → a
Equations
- a.mkFuncsRev tys = List.foldl (fun (cur s : Auto.Embedding.Lam.LamSort) => s.func cur) a tys
Instances For
Given ty₀ → ty₁ → ⋯ → tyᵢ₋₁ → a
, return a
Equations
Instances For
Given ty₀ → ty₁ → ⋯ → tyₙ₋₁ → a
, return [ty₀, ty₁, ⋯, tyₙ₋₁]
Equations
- Auto.Embedding.Lam.LamSort.getArgTysN Nat.zero s = some []
- Auto.Embedding.Lam.LamSort.getArgTysN n_2.succ (a.func a_1) = (Auto.Embedding.Lam.LamSort.getArgTysN n_2 a_1).bind fun (x : List Auto.Embedding.Lam.LamSort) => some (a :: x)
- Auto.Embedding.Lam.LamSort.getArgTysN n_2.succ s = none
Instances For
Given ty₀ → ty₁ → ⋯ → tyₙ₋₁ → a
, return a
Equations
Instances For
Equations
- Auto.Embedding.Lam.LamSort.interp val (Auto.Embedding.Lam.LamSort.atom a) = val a
- Auto.Embedding.Lam.LamSort.interp val (Auto.Embedding.Lam.LamSort.base a) = a.interp
- Auto.Embedding.Lam.LamSort.interp val (a.func a_1) = (Auto.Embedding.Lam.LamSort.interp val a → Auto.Embedding.Lam.LamSort.interp val a_1)
Instances For
Equations
- One or more equations did not get rendered due to their size.
- Auto.Embedding.Lam.LamSort.curry f_2 = f_2 Auto.HList.nil
Instances For
Equations
- One or more equations did not get rendered due to their size.
- Auto.Embedding.Lam.LamSort.curryRev f_2 = f_2 Auto.HList.nil
Instances For
Equations
Equations
- Auto.Embedding.Lam.instToExprPropConst = { toExpr := Auto.Embedding.Lam.toExprPropConst✝, toTypeExpr := Lean.Expr.const `Auto.Embedding.Lam.PropConst [] }
Equations
- Auto.Embedding.Lam.PropConst.trueE.reprAux = "trueE"
- Auto.Embedding.Lam.PropConst.falseE.reprAux = "falseE"
- Auto.Embedding.Lam.PropConst.not.reprAux = "not"
- Auto.Embedding.Lam.PropConst.and.reprAux = "and"
- Auto.Embedding.Lam.PropConst.or.reprAux = "or"
- Auto.Embedding.Lam.PropConst.imp.reprAux = "imp"
- Auto.Embedding.Lam.PropConst.iff.reprAux = "iff"
Instances For
Equations
- p.reprPrec 0 = Std.format "Auto.Embedding.Lam.PropConst." ++ Std.format p.reprAux ++ Std.format ""
- p.reprPrec n_2.succ = Std.format "(" ++ Std.format p.reprAux ++ Std.format ")"
Instances For
Equations
Equations
- Auto.Embedding.Lam.PropConst.trueE.toString = "True"
- Auto.Embedding.Lam.PropConst.falseE.toString = "False"
- Auto.Embedding.Lam.PropConst.not.toString = "¬"
- Auto.Embedding.Lam.PropConst.and.toString = "∧"
- Auto.Embedding.Lam.PropConst.or.toString = "∨"
- Auto.Embedding.Lam.PropConst.imp.toString = "→"
- Auto.Embedding.Lam.PropConst.iff.toString = "↔"
Instances For
Equations
Equations
- Auto.Embedding.Lam.PropConst.trueE.beq Auto.Embedding.Lam.PropConst.trueE = true
- Auto.Embedding.Lam.PropConst.falseE.beq Auto.Embedding.Lam.PropConst.falseE = true
- Auto.Embedding.Lam.PropConst.not.beq Auto.Embedding.Lam.PropConst.not = true
- Auto.Embedding.Lam.PropConst.and.beq Auto.Embedding.Lam.PropConst.and = true
- Auto.Embedding.Lam.PropConst.or.beq Auto.Embedding.Lam.PropConst.or = true
- Auto.Embedding.Lam.PropConst.imp.beq Auto.Embedding.Lam.PropConst.imp = true
- Auto.Embedding.Lam.PropConst.iff.beq Auto.Embedding.Lam.PropConst.iff = true
- x✝¹.beq x✝ = false
Instances For
Equations
Equations
- One or more equations did not get rendered due to their size.
- Auto.Embedding.Lam.PropConst.trueE.lamCheck = Auto.Embedding.Lam.LamSort.base Auto.Embedding.Lam.LamBaseSort.prop
- Auto.Embedding.Lam.PropConst.falseE.lamCheck = Auto.Embedding.Lam.LamSort.base Auto.Embedding.Lam.LamBaseSort.prop
- Auto.Embedding.Lam.PropConst.not.lamCheck = (Auto.Embedding.Lam.LamSort.base Auto.Embedding.Lam.LamBaseSort.prop).func (Auto.Embedding.Lam.LamSort.base Auto.Embedding.Lam.LamBaseSort.prop)
Instances For
- ofTrueE : trueE.LamWF (LamSort.base LamBaseSort.prop)
- ofFalseE : falseE.LamWF (LamSort.base LamBaseSort.prop)
- ofNot : not.LamWF ((LamSort.base LamBaseSort.prop).func (LamSort.base LamBaseSort.prop))
- ofAnd : and.LamWF ((LamSort.base LamBaseSort.prop).func ((LamSort.base LamBaseSort.prop).func (LamSort.base LamBaseSort.prop)))
- ofOr : or.LamWF ((LamSort.base LamBaseSort.prop).func ((LamSort.base LamBaseSort.prop).func (LamSort.base LamBaseSort.prop)))
- ofImp : imp.LamWF ((LamSort.base LamBaseSort.prop).func ((LamSort.base LamBaseSort.prop).func (LamSort.base LamBaseSort.prop)))
- ofIff : iff.LamWF ((LamSort.base LamBaseSort.prop).func ((LamSort.base LamBaseSort.prop).func (LamSort.base LamBaseSort.prop)))
Instances For
Equations
- One or more equations did not get rendered due to their size.
- Auto.Embedding.Lam.PropConst.LamWF.ofPropConst Auto.Embedding.Lam.PropConst.trueE = ⟨Auto.Embedding.Lam.LamSort.base Auto.Embedding.Lam.LamBaseSort.prop, Auto.Embedding.Lam.PropConst.LamWF.ofTrueE⟩
Instances For
Equations
- ⋯ = ⋯
Instances For
Equations
Equations
- Auto.Embedding.Lam.instToExprBoolConst = { toExpr := Auto.Embedding.Lam.toExprBoolConst✝, toTypeExpr := Lean.Expr.const `Auto.Embedding.Lam.BoolConst [] }
Equations
- Auto.Embedding.Lam.BoolConst.ofProp.reprAux = "ofProp"
- Auto.Embedding.Lam.BoolConst.trueb.reprAux = "trueb"
- Auto.Embedding.Lam.BoolConst.falseb.reprAux = "falseb"
- Auto.Embedding.Lam.BoolConst.notb.reprAux = "notb"
- Auto.Embedding.Lam.BoolConst.andb.reprAux = "andb"
- Auto.Embedding.Lam.BoolConst.orb.reprAux = "orb"
Instances For
Equations
- b.reprPrec 0 = Std.format "Auto.Embedding.Lam.BoolConst." ++ Std.format b.reprAux ++ Std.format ""
- b.reprPrec n_2.succ = Std.format "(." ++ Std.format b.reprAux ++ Std.format ")"
Instances For
Equations
Equations
- Auto.Embedding.Lam.BoolConst.ofProp.toString = "ofProp"
- Auto.Embedding.Lam.BoolConst.trueb.toString = "true"
- Auto.Embedding.Lam.BoolConst.falseb.toString = "false"
- Auto.Embedding.Lam.BoolConst.notb.toString = "!"
- Auto.Embedding.Lam.BoolConst.andb.toString = "&&"
- Auto.Embedding.Lam.BoolConst.orb.toString = "||"
Instances For
Equations
Equations
- Auto.Embedding.Lam.BoolConst.ofProp.beq Auto.Embedding.Lam.BoolConst.ofProp = true
- Auto.Embedding.Lam.BoolConst.trueb.beq Auto.Embedding.Lam.BoolConst.trueb = true
- Auto.Embedding.Lam.BoolConst.falseb.beq Auto.Embedding.Lam.BoolConst.falseb = true
- Auto.Embedding.Lam.BoolConst.notb.beq Auto.Embedding.Lam.BoolConst.notb = true
- Auto.Embedding.Lam.BoolConst.andb.beq Auto.Embedding.Lam.BoolConst.andb = true
- Auto.Embedding.Lam.BoolConst.orb.beq Auto.Embedding.Lam.BoolConst.orb = true
- x✝¹.beq x✝ = false
Instances For
Equations
Equations
- One or more equations did not get rendered due to their size.
- Auto.Embedding.Lam.BoolConst.ofProp.lamCheck = (Auto.Embedding.Lam.LamSort.base Auto.Embedding.Lam.LamBaseSort.prop).func (Auto.Embedding.Lam.LamSort.base Auto.Embedding.Lam.LamBaseSort.bool)
- Auto.Embedding.Lam.BoolConst.trueb.lamCheck = Auto.Embedding.Lam.LamSort.base Auto.Embedding.Lam.LamBaseSort.bool
- Auto.Embedding.Lam.BoolConst.falseb.lamCheck = Auto.Embedding.Lam.LamSort.base Auto.Embedding.Lam.LamBaseSort.bool
- Auto.Embedding.Lam.BoolConst.notb.lamCheck = (Auto.Embedding.Lam.LamSort.base Auto.Embedding.Lam.LamBaseSort.bool).func (Auto.Embedding.Lam.LamSort.base Auto.Embedding.Lam.LamBaseSort.bool)
Instances For
- ofOfProp : ofProp.LamWF ((LamSort.base LamBaseSort.prop).func (LamSort.base LamBaseSort.bool))
- ofTrueB : trueb.LamWF (LamSort.base LamBaseSort.bool)
- ofFalseB : falseb.LamWF (LamSort.base LamBaseSort.bool)
- ofNotB : notb.LamWF ((LamSort.base LamBaseSort.bool).func (LamSort.base LamBaseSort.bool))
- ofAndB : andb.LamWF ((LamSort.base LamBaseSort.bool).func ((LamSort.base LamBaseSort.bool).func (LamSort.base LamBaseSort.bool)))
- ofOrB : orb.LamWF ((LamSort.base LamBaseSort.bool).func ((LamSort.base LamBaseSort.bool).func (LamSort.base LamBaseSort.bool)))
Instances For
Equations
- One or more equations did not get rendered due to their size.
- Auto.Embedding.Lam.BoolConst.LamWF.ofBoolConst Auto.Embedding.Lam.BoolConst.trueb = ⟨Auto.Embedding.Lam.LamSort.base Auto.Embedding.Lam.LamBaseSort.bool, Auto.Embedding.Lam.BoolConst.LamWF.ofTrueB⟩
Instances For
Equations
- ⋯ = ⋯
Instances For
Equations
Equations
- Auto.Embedding.Lam.instToExprNatConst = { toExpr := Auto.Embedding.Lam.toExprNatConst✝, toTypeExpr := Lean.Expr.const `Auto.Embedding.Lam.NatConst [] }
Equations
- (Auto.Embedding.Lam.NatConst.natVal a).reprAux = toString "natVal " ++ toString a ++ toString ""
- Auto.Embedding.Lam.NatConst.nadd.reprAux = "nadd"
- Auto.Embedding.Lam.NatConst.nsub.reprAux = "nsub"
- Auto.Embedding.Lam.NatConst.nmul.reprAux = "nmul"
- Auto.Embedding.Lam.NatConst.ndiv.reprAux = "ndiv"
- Auto.Embedding.Lam.NatConst.nmod.reprAux = "nmod"
- Auto.Embedding.Lam.NatConst.nle.reprAux = "nle"
- Auto.Embedding.Lam.NatConst.nlt.reprAux = "nlt"
- Auto.Embedding.Lam.NatConst.nmax.reprAux = "nmax"
- Auto.Embedding.Lam.NatConst.nmin.reprAux = "nmin"
Instances For
Equations
- nc.reprPrec 0 = Std.format "Auto.Embedding.Lam.NatConst." ++ Std.format nc.reprAux ++ Std.format ""
- nc.reprPrec n_2.succ = Std.format "(." ++ Std.format nc.reprAux ++ Std.format ")"
Instances For
Equations
Equations
- (Auto.Embedding.Lam.NatConst.natVal a).toString = toString "" ++ toString a ++ toString " : Nat"
- Auto.Embedding.Lam.NatConst.nadd.toString = "+"
- Auto.Embedding.Lam.NatConst.nsub.toString = "-"
- Auto.Embedding.Lam.NatConst.nmul.toString = "*"
- Auto.Embedding.Lam.NatConst.ndiv.toString = "/"
- Auto.Embedding.Lam.NatConst.nmod.toString = "%"
- Auto.Embedding.Lam.NatConst.nle.toString = "≤"
- Auto.Embedding.Lam.NatConst.nlt.toString = "<"
- Auto.Embedding.Lam.NatConst.nmax.toString = "nmax"
- Auto.Embedding.Lam.NatConst.nmin.toString = "nmin"
Instances For
Equations
Equations
- (Auto.Embedding.Lam.NatConst.natVal n).beq (Auto.Embedding.Lam.NatConst.natVal m) = n.beq m
- Auto.Embedding.Lam.NatConst.nadd.beq Auto.Embedding.Lam.NatConst.nadd = true
- Auto.Embedding.Lam.NatConst.nsub.beq Auto.Embedding.Lam.NatConst.nsub = true
- Auto.Embedding.Lam.NatConst.nmul.beq Auto.Embedding.Lam.NatConst.nmul = true
- Auto.Embedding.Lam.NatConst.ndiv.beq Auto.Embedding.Lam.NatConst.ndiv = true
- Auto.Embedding.Lam.NatConst.nmod.beq Auto.Embedding.Lam.NatConst.nmod = true
- Auto.Embedding.Lam.NatConst.nle.beq Auto.Embedding.Lam.NatConst.nle = true
- Auto.Embedding.Lam.NatConst.nlt.beq Auto.Embedding.Lam.NatConst.nlt = true
- Auto.Embedding.Lam.NatConst.nmax.beq Auto.Embedding.Lam.NatConst.nmax = true
- Auto.Embedding.Lam.NatConst.nmin.beq Auto.Embedding.Lam.NatConst.nmin = true
- x✝¹.beq x✝ = false
Instances For
Equations
Equations
- One or more equations did not get rendered due to their size.
- (Auto.Embedding.Lam.NatConst.natVal a).lamCheck = Auto.Embedding.Lam.LamSort.base Auto.Embedding.Lam.LamBaseSort.nat
Instances For
- ofNatVal (n : Nat) : (natVal n).LamWF (LamSort.base LamBaseSort.nat)
- ofNadd : nadd.LamWF ((LamSort.base LamBaseSort.nat).func ((LamSort.base LamBaseSort.nat).func (LamSort.base LamBaseSort.nat)))
- ofNsub : nsub.LamWF ((LamSort.base LamBaseSort.nat).func ((LamSort.base LamBaseSort.nat).func (LamSort.base LamBaseSort.nat)))
- ofNmul : nmul.LamWF ((LamSort.base LamBaseSort.nat).func ((LamSort.base LamBaseSort.nat).func (LamSort.base LamBaseSort.nat)))
- ofNdiv : ndiv.LamWF ((LamSort.base LamBaseSort.nat).func ((LamSort.base LamBaseSort.nat).func (LamSort.base LamBaseSort.nat)))
- ofNmod : nmod.LamWF ((LamSort.base LamBaseSort.nat).func ((LamSort.base LamBaseSort.nat).func (LamSort.base LamBaseSort.nat)))
- ofNle : nle.LamWF ((LamSort.base LamBaseSort.nat).func ((LamSort.base LamBaseSort.nat).func (LamSort.base LamBaseSort.prop)))
- ofNlt : nlt.LamWF ((LamSort.base LamBaseSort.nat).func ((LamSort.base LamBaseSort.nat).func (LamSort.base LamBaseSort.prop)))
- ofNmax : nmax.LamWF ((LamSort.base LamBaseSort.nat).func ((LamSort.base LamBaseSort.nat).func (LamSort.base LamBaseSort.nat)))
- ofNmin : nmin.LamWF ((LamSort.base LamBaseSort.nat).func ((LamSort.base LamBaseSort.nat).func (LamSort.base LamBaseSort.nat)))
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- ⋯ = ⋯
Instances For
Equations
Equations
- Auto.Embedding.Lam.instToExprIntConst = { toExpr := Auto.Embedding.Lam.toExprIntConst✝, toTypeExpr := Lean.Expr.const `Auto.Embedding.Lam.IntConst [] }
Equations
- Auto.Embedding.Lam.IntConst.iofNat.reprAux = "iofNat"
- Auto.Embedding.Lam.IntConst.inegSucc.reprAux = "inegSucc"
- Auto.Embedding.Lam.IntConst.ineg.reprAux = "ineg"
- Auto.Embedding.Lam.IntConst.iabs.reprAux = "iabs"
- Auto.Embedding.Lam.IntConst.iadd.reprAux = "iadd"
- Auto.Embedding.Lam.IntConst.isub.reprAux = "isub"
- Auto.Embedding.Lam.IntConst.imul.reprAux = "imul"
- Auto.Embedding.Lam.IntConst.idiv.reprAux = "idiv"
- Auto.Embedding.Lam.IntConst.imod.reprAux = "imod"
- Auto.Embedding.Lam.IntConst.iediv.reprAux = "iediv"
- Auto.Embedding.Lam.IntConst.iemod.reprAux = "iemod"
- Auto.Embedding.Lam.IntConst.ile.reprAux = "ile"
- Auto.Embedding.Lam.IntConst.ilt.reprAux = "ilt"
- Auto.Embedding.Lam.IntConst.imax.reprAux = "imax"
- Auto.Embedding.Lam.IntConst.imin.reprAux = "imin"
Instances For
Equations
- i.reprPrec 0 = Std.format "Auto.Embedding.Lam.IntConst." ++ Std.format i.reprAux ++ Std.format ""
- i.reprPrec n_2.succ = Std.format "(." ++ Std.format i.reprAux ++ Std.format ")"
Instances For
Equations
Equations
- Auto.Embedding.Lam.IntConst.iofNat.toString = "iofNat"
- Auto.Embedding.Lam.IntConst.inegSucc.toString = "inegSucc"
- Auto.Embedding.Lam.IntConst.ineg.toString = "-"
- Auto.Embedding.Lam.IntConst.iabs.toString = "iabs"
- Auto.Embedding.Lam.IntConst.iadd.toString = "+"
- Auto.Embedding.Lam.IntConst.isub.toString = "-"
- Auto.Embedding.Lam.IntConst.imul.toString = "*"
- Auto.Embedding.Lam.IntConst.idiv.toString = "/"
- Auto.Embedding.Lam.IntConst.imod.toString = "%"
- Auto.Embedding.Lam.IntConst.iediv.toString = "/?"
- Auto.Embedding.Lam.IntConst.iemod.toString = "%?"
- Auto.Embedding.Lam.IntConst.ile.toString = "≤"
- Auto.Embedding.Lam.IntConst.ilt.toString = "<"
- Auto.Embedding.Lam.IntConst.imax.toString = "imax"
- Auto.Embedding.Lam.IntConst.imin.toString = "imin"
Instances For
Equations
Equations
- Auto.Embedding.Lam.IntConst.iofNat.beq Auto.Embedding.Lam.IntConst.iofNat = true
- Auto.Embedding.Lam.IntConst.inegSucc.beq Auto.Embedding.Lam.IntConst.inegSucc = true
- Auto.Embedding.Lam.IntConst.ineg.beq Auto.Embedding.Lam.IntConst.ineg = true
- Auto.Embedding.Lam.IntConst.iabs.beq Auto.Embedding.Lam.IntConst.iabs = true
- Auto.Embedding.Lam.IntConst.iadd.beq Auto.Embedding.Lam.IntConst.iadd = true
- Auto.Embedding.Lam.IntConst.isub.beq Auto.Embedding.Lam.IntConst.isub = true
- Auto.Embedding.Lam.IntConst.imul.beq Auto.Embedding.Lam.IntConst.imul = true
- Auto.Embedding.Lam.IntConst.idiv.beq Auto.Embedding.Lam.IntConst.idiv = true
- Auto.Embedding.Lam.IntConst.imod.beq Auto.Embedding.Lam.IntConst.imod = true
- Auto.Embedding.Lam.IntConst.iediv.beq Auto.Embedding.Lam.IntConst.iediv = true
- Auto.Embedding.Lam.IntConst.iemod.beq Auto.Embedding.Lam.IntConst.iemod = true
- Auto.Embedding.Lam.IntConst.ile.beq Auto.Embedding.Lam.IntConst.ile = true
- Auto.Embedding.Lam.IntConst.ilt.beq Auto.Embedding.Lam.IntConst.ilt = true
- Auto.Embedding.Lam.IntConst.imax.beq Auto.Embedding.Lam.IntConst.imax = true
- Auto.Embedding.Lam.IntConst.imin.beq Auto.Embedding.Lam.IntConst.imin = true
- x✝¹.beq x✝ = false
Instances For
Equations
Equations
- One or more equations did not get rendered due to their size.
- Auto.Embedding.Lam.IntConst.iofNat.lamCheck = (Auto.Embedding.Lam.LamSort.base Auto.Embedding.Lam.LamBaseSort.nat).func (Auto.Embedding.Lam.LamSort.base Auto.Embedding.Lam.LamBaseSort.int)
- Auto.Embedding.Lam.IntConst.inegSucc.lamCheck = (Auto.Embedding.Lam.LamSort.base Auto.Embedding.Lam.LamBaseSort.nat).func (Auto.Embedding.Lam.LamSort.base Auto.Embedding.Lam.LamBaseSort.int)
- Auto.Embedding.Lam.IntConst.ineg.lamCheck = (Auto.Embedding.Lam.LamSort.base Auto.Embedding.Lam.LamBaseSort.int).func (Auto.Embedding.Lam.LamSort.base Auto.Embedding.Lam.LamBaseSort.int)
- Auto.Embedding.Lam.IntConst.iabs.lamCheck = (Auto.Embedding.Lam.LamSort.base Auto.Embedding.Lam.LamBaseSort.int).func (Auto.Embedding.Lam.LamSort.base Auto.Embedding.Lam.LamBaseSort.int)
Instances For
- ofIOfNat : iofNat.LamWF ((LamSort.base LamBaseSort.nat).func (LamSort.base LamBaseSort.int))
- ofINegSucc : inegSucc.LamWF ((LamSort.base LamBaseSort.nat).func (LamSort.base LamBaseSort.int))
- ofIneg : ineg.LamWF ((LamSort.base LamBaseSort.int).func (LamSort.base LamBaseSort.int))
- ofIabs : iabs.LamWF ((LamSort.base LamBaseSort.int).func (LamSort.base LamBaseSort.int))
- ofIadd : iadd.LamWF ((LamSort.base LamBaseSort.int).func ((LamSort.base LamBaseSort.int).func (LamSort.base LamBaseSort.int)))
- ofIsub : isub.LamWF ((LamSort.base LamBaseSort.int).func ((LamSort.base LamBaseSort.int).func (LamSort.base LamBaseSort.int)))
- ofImul : imul.LamWF ((LamSort.base LamBaseSort.int).func ((LamSort.base LamBaseSort.int).func (LamSort.base LamBaseSort.int)))
- ofIdiv : idiv.LamWF ((LamSort.base LamBaseSort.int).func ((LamSort.base LamBaseSort.int).func (LamSort.base LamBaseSort.int)))
- ofImod : imod.LamWF ((LamSort.base LamBaseSort.int).func ((LamSort.base LamBaseSort.int).func (LamSort.base LamBaseSort.int)))
- ofIediv : iediv.LamWF ((LamSort.base LamBaseSort.int).func ((LamSort.base LamBaseSort.int).func (LamSort.base LamBaseSort.int)))
- ofIemod : iemod.LamWF ((LamSort.base LamBaseSort.int).func ((LamSort.base LamBaseSort.int).func (LamSort.base LamBaseSort.int)))
- ofIle : ile.LamWF ((LamSort.base LamBaseSort.int).func ((LamSort.base LamBaseSort.int).func (LamSort.base LamBaseSort.prop)))
- ofIlt : ilt.LamWF ((LamSort.base LamBaseSort.int).func ((LamSort.base LamBaseSort.int).func (LamSort.base LamBaseSort.prop)))
- ofImax : imax.LamWF ((LamSort.base LamBaseSort.int).func ((LamSort.base LamBaseSort.int).func (LamSort.base LamBaseSort.int)))
- ofImin : imin.LamWF ((LamSort.base LamBaseSort.int).func ((LamSort.base LamBaseSort.int).func (LamSort.base LamBaseSort.int)))
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- ⋯ = ⋯
Instances For
- strVal (s : String) : StringConst
- slength : StringConst
- sapp : StringConst
- sle : StringConst
- slt : StringConst
- sprefixof : StringConst
- srepall : StringConst
Instances For
Equations
- Auto.Embedding.Lam.instToExprStringConst = { toExpr := Auto.Embedding.Lam.toExprStringConst✝, toTypeExpr := Lean.Expr.const `Auto.Embedding.Lam.StringConst [] }
Equations
- (Auto.Embedding.Lam.StringConst.strVal a).reprAux = toString "strVal \"" ++ toString a ++ toString "\""
- Auto.Embedding.Lam.StringConst.slength.reprAux = "slength"
- Auto.Embedding.Lam.StringConst.sapp.reprAux = "sapp"
- Auto.Embedding.Lam.StringConst.sle.reprAux = "sle"
- Auto.Embedding.Lam.StringConst.slt.reprAux = "slt"
- Auto.Embedding.Lam.StringConst.sprefixof.reprAux = "sprefixof"
- Auto.Embedding.Lam.StringConst.srepall.reprAux = "srepall"
Instances For
Equations
- s.reprPrec 0 = Std.format "Auto.Embedding.Lam.StringConst." ++ Std.format s.reprAux ++ Std.format ""
- s.reprPrec n_2.succ = Std.format "(." ++ Std.format s.reprAux ++ Std.format ")"
Instances For
Equations
Equations
- (Auto.Embedding.Lam.StringConst.strVal a).toString = toString "(" ++ toString a ++ toString " : String)"
- Auto.Embedding.Lam.StringConst.slength.toString = "length"
- Auto.Embedding.Lam.StringConst.sapp.toString = "++"
- Auto.Embedding.Lam.StringConst.sle.toString = "≤"
- Auto.Embedding.Lam.StringConst.slt.toString = "<"
- Auto.Embedding.Lam.StringConst.sprefixof.toString = "is_prefix_of"
- Auto.Embedding.Lam.StringConst.srepall.toString = "replace_all"
Instances For
Equations
- (Auto.Embedding.Lam.StringConst.strVal m).beq (Auto.Embedding.Lam.StringConst.strVal n) = (m == n)
- Auto.Embedding.Lam.StringConst.slength.beq Auto.Embedding.Lam.StringConst.slength = true
- Auto.Embedding.Lam.StringConst.sapp.beq Auto.Embedding.Lam.StringConst.sapp = true
- Auto.Embedding.Lam.StringConst.sle.beq Auto.Embedding.Lam.StringConst.sle = true
- Auto.Embedding.Lam.StringConst.slt.beq Auto.Embedding.Lam.StringConst.slt = true
- Auto.Embedding.Lam.StringConst.sprefixof.beq Auto.Embedding.Lam.StringConst.sprefixof = true
- Auto.Embedding.Lam.StringConst.srepall.beq Auto.Embedding.Lam.StringConst.srepall = true
- x✝¹.beq x✝ = false
Instances For
Equations
- ⋯ = ⋯
Instances For
Equations
- ⋯ = ⋯
Instances For
Equations
- One or more equations did not get rendered due to their size.
- (Auto.Embedding.Lam.StringConst.strVal a).lamCheck = Auto.Embedding.Lam.LamSort.base Auto.Embedding.Lam.LamBaseSort.string
Instances For
- ofStrVal (s : String) : (strVal s).LamWF (LamSort.base LamBaseSort.string)
- ofSlength : slength.LamWF ((LamSort.base LamBaseSort.string).func (LamSort.base LamBaseSort.nat))
- ofSapp : sapp.LamWF ((LamSort.base LamBaseSort.string).func ((LamSort.base LamBaseSort.string).func (LamSort.base LamBaseSort.string)))
- ofSle : sle.LamWF ((LamSort.base LamBaseSort.string).func ((LamSort.base LamBaseSort.string).func (LamSort.base LamBaseSort.prop)))
- ofSlt : slt.LamWF ((LamSort.base LamBaseSort.string).func ((LamSort.base LamBaseSort.string).func (LamSort.base LamBaseSort.prop)))
- ofSprefixof : sprefixof.LamWF ((LamSort.base LamBaseSort.string).func ((LamSort.base LamBaseSort.string).func (LamSort.base LamBaseSort.bool)))
- ofSrepall : srepall.LamWF ((LamSort.base LamBaseSort.string).func ((LamSort.base LamBaseSort.string).func ((LamSort.base LamBaseSort.string).func (LamSort.base LamBaseSort.string))))
Instances For
Equations
- ⋯ = ⋯
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- ⋯ = ⋯
Instances For
Equations
- ⋯ = ⋯
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Equations
Equations
- Auto.Embedding.Lam.instToExprBVAOp = { toExpr := Auto.Embedding.Lam.toExprBVAOp✝, toTypeExpr := Lean.Expr.const `Auto.Embedding.Lam.BVAOp [] }
Equations
- Auto.Embedding.Lam.BVAOp.repr n Auto.Embedding.Lam.BVAOp.add = toString "bvadd " ++ toString n ++ toString ""
- Auto.Embedding.Lam.BVAOp.repr n Auto.Embedding.Lam.BVAOp.sub = toString "bvsub " ++ toString n ++ toString ""
- Auto.Embedding.Lam.BVAOp.repr n Auto.Embedding.Lam.BVAOp.mul = toString "bvmul " ++ toString n ++ toString ""
- Auto.Embedding.Lam.BVAOp.repr n Auto.Embedding.Lam.BVAOp.udiv = toString "bvudiv " ++ toString n ++ toString ""
- Auto.Embedding.Lam.BVAOp.repr n Auto.Embedding.Lam.BVAOp.urem = toString "bvurem " ++ toString n ++ toString ""
- Auto.Embedding.Lam.BVAOp.repr n Auto.Embedding.Lam.BVAOp.sdiv = toString "bvsdiv " ++ toString n ++ toString ""
- Auto.Embedding.Lam.BVAOp.repr n Auto.Embedding.Lam.BVAOp.srem = toString "bvsrem " ++ toString n ++ toString ""
- Auto.Embedding.Lam.BVAOp.repr n Auto.Embedding.Lam.BVAOp.smod = toString "bvsmod " ++ toString n ++ toString ""
Instances For
Equations
- Auto.Embedding.Lam.BVAOp.add.toString = toString "+"
- Auto.Embedding.Lam.BVAOp.sub.toString = toString "-"
- Auto.Embedding.Lam.BVAOp.mul.toString = toString "*"
- Auto.Embedding.Lam.BVAOp.udiv.toString = toString "/ᵤ"
- Auto.Embedding.Lam.BVAOp.urem.toString = toString "%ᵤ"
- Auto.Embedding.Lam.BVAOp.sdiv.toString = toString "/"
- Auto.Embedding.Lam.BVAOp.srem.toString = toString "%ᵣ"
- Auto.Embedding.Lam.BVAOp.smod.toString = toString "%"
Instances For
Equations
- Auto.Embedding.Lam.BVAOp.add.beq Auto.Embedding.Lam.BVAOp.add = true
- Auto.Embedding.Lam.BVAOp.sub.beq Auto.Embedding.Lam.BVAOp.sub = true
- Auto.Embedding.Lam.BVAOp.mul.beq Auto.Embedding.Lam.BVAOp.mul = true
- Auto.Embedding.Lam.BVAOp.udiv.beq Auto.Embedding.Lam.BVAOp.udiv = true
- Auto.Embedding.Lam.BVAOp.urem.beq Auto.Embedding.Lam.BVAOp.urem = true
- Auto.Embedding.Lam.BVAOp.sdiv.beq Auto.Embedding.Lam.BVAOp.sdiv = true
- Auto.Embedding.Lam.BVAOp.srem.beq Auto.Embedding.Lam.BVAOp.srem = true
- Auto.Embedding.Lam.BVAOp.smod.beq Auto.Embedding.Lam.BVAOp.smod = true
- x✝¹.beq x✝ = false
Instances For
Equations
Equations
Equations
Equations
- Auto.Embedding.Lam.instToExprBVCmp = { toExpr := Auto.Embedding.Lam.toExprBVCmp✝, toTypeExpr := Lean.Expr.const `Auto.Embedding.Lam.BVCmp [] }
Equations
- Auto.Embedding.Lam.BVCmp.repr n prop? Auto.Embedding.Lam.BVCmp.ult = toString "bv" ++ toString (if prop? = true then "p" else "") ++ toString "ult " ++ toString n ++ toString ""
- Auto.Embedding.Lam.BVCmp.repr n prop? Auto.Embedding.Lam.BVCmp.ule = toString "bv" ++ toString (if prop? = true then "p" else "") ++ toString "ule " ++ toString n ++ toString ""
- Auto.Embedding.Lam.BVCmp.repr n prop? Auto.Embedding.Lam.BVCmp.slt = toString "bv" ++ toString (if prop? = true then "p" else "") ++ toString "slt " ++ toString n ++ toString ""
- Auto.Embedding.Lam.BVCmp.repr n prop? Auto.Embedding.Lam.BVCmp.sle = toString "bv" ++ toString (if prop? = true then "p" else "") ++ toString "sle " ++ toString n ++ toString ""
Instances For
Equations
- Auto.Embedding.Lam.BVCmp.toString prop? Auto.Embedding.Lam.BVCmp.ult = toString "" ++ toString (if prop? = true then "ₚ" else "") ++ toString "<ᵤ"
- Auto.Embedding.Lam.BVCmp.toString prop? Auto.Embedding.Lam.BVCmp.ule = toString "" ++ toString (if prop? = true then "ₚ" else "") ++ toString "≤ᵤ"
- Auto.Embedding.Lam.BVCmp.toString prop? Auto.Embedding.Lam.BVCmp.slt = toString "" ++ toString (if prop? = true then "ₚ" else "") ++ toString "<"
- Auto.Embedding.Lam.BVCmp.toString prop? Auto.Embedding.Lam.BVCmp.sle = toString "" ++ toString (if prop? = true then "ₚ" else "") ++ toString "≤"
Instances For
Equations
Instances For
Equations
Equations
Equations
Equations
- Auto.Embedding.Lam.instToExprBVShOp = { toExpr := Auto.Embedding.Lam.toExprBVShOp✝, toTypeExpr := Lean.Expr.const `Auto.Embedding.Lam.BVShOp [] }
Equations
- Auto.Embedding.Lam.BVShOp.repr n smt? Auto.Embedding.Lam.BVShOp.shl = toString "bv" ++ toString (if smt? = true then "smt" else "") ++ toString "shl " ++ toString n ++ toString ""
- Auto.Embedding.Lam.BVShOp.repr n smt? Auto.Embedding.Lam.BVShOp.lshr = toString "bv" ++ toString (if smt? = true then "smt" else "") ++ toString "lshr " ++ toString n ++ toString ""
- Auto.Embedding.Lam.BVShOp.repr n smt? Auto.Embedding.Lam.BVShOp.ashr = toString "bv" ++ toString (if smt? = true then "smt" else "") ++ toString "ashr " ++ toString n ++ toString ""
Instances For
Equations
- Auto.Embedding.Lam.BVShOp.toString smt? Auto.Embedding.Lam.BVShOp.shl = toString "<<<" ++ toString (if smt? = true then "ₛ" else "") ++ toString ""
- Auto.Embedding.Lam.BVShOp.toString smt? Auto.Embedding.Lam.BVShOp.lshr = toString ">>>" ++ toString (if smt? = true then "ₛ" else "") ++ toString ""
- Auto.Embedding.Lam.BVShOp.toString smt? Auto.Embedding.Lam.BVShOp.ashr = toString ">>>ₐ" ++ toString (if smt? = true then "ₛ" else "") ++ toString ""
Instances For
Equations
Instances For
Equations
Following https://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV
- bvVal (n i : Nat) : BitVecConst
- bvofNat (n : Nat) : BitVecConst
- bvtoNat (n : Nat) : BitVecConst
- bvofInt (n : Nat) : BitVecConst
- bvtoInt (n : Nat) : BitVecConst
- bvmsb (n : Nat) : BitVecConst
- bvaOp (n : Nat) (op : BVAOp) : BitVecConst
- bvneg (n : Nat) : BitVecConst
- bvabs (n : Nat) : BitVecConst
- bvcmp (n : Nat) (prop? : Bool) (op : BVCmp) : BitVecConst
- bvand (n : Nat) : BitVecConst
- bvor (n : Nat) : BitVecConst
- bvxor (n : Nat) : BitVecConst
- bvnot (n : Nat) : BitVecConst
- bvshOp (n : Nat) (smt? : Bool) (op : BVShOp) : BitVecConst
- bvappend (n m : Nat) : BitVecConst
- bvextract (n hi lo : Nat) : BitVecConst
- bvrepeat (w i : Nat) : BitVecConst
- bvzeroExtend (w v : Nat) : BitVecConst
- bvsignExtend (w v : Nat) : BitVecConst
Instances For
Equations
- Auto.Embedding.Lam.instToExprBitVecConst = { toExpr := Auto.Embedding.Lam.toExprBitVecConst✝, toTypeExpr := Lean.Expr.const `Auto.Embedding.Lam.BitVecConst [] }
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
- (Auto.Embedding.Lam.BitVecConst.bvVal a a_1).reprAux = toString "bvVal " ++ toString a ++ toString " " ++ toString a_1 ++ toString ""
- (Auto.Embedding.Lam.BitVecConst.bvofNat a).reprAux = toString "bvofNat " ++ toString a ++ toString ""
- (Auto.Embedding.Lam.BitVecConst.bvtoNat a).reprAux = toString "bvtoNat " ++ toString a ++ toString ""
- (Auto.Embedding.Lam.BitVecConst.bvofInt a).reprAux = toString "bvofInt " ++ toString a ++ toString ""
- (Auto.Embedding.Lam.BitVecConst.bvtoInt a).reprAux = toString "bvtoInt " ++ toString a ++ toString ""
- (Auto.Embedding.Lam.BitVecConst.bvmsb a).reprAux = toString "bvmsb " ++ toString a ++ toString ""
- (Auto.Embedding.Lam.BitVecConst.bvaOp a a_1).reprAux = Auto.Embedding.Lam.BVAOp.repr a a_1
- (Auto.Embedding.Lam.BitVecConst.bvneg a).reprAux = toString "bvneg " ++ toString a ++ toString ""
- (Auto.Embedding.Lam.BitVecConst.bvabs a).reprAux = toString "bvabs " ++ toString a ++ toString ""
- (Auto.Embedding.Lam.BitVecConst.bvcmp a a_1 a_2).reprAux = Auto.Embedding.Lam.BVCmp.repr a a_1 a_2
- (Auto.Embedding.Lam.BitVecConst.bvand a).reprAux = toString "bvand " ++ toString a ++ toString ""
- (Auto.Embedding.Lam.BitVecConst.bvor a).reprAux = toString "bvor " ++ toString a ++ toString ""
- (Auto.Embedding.Lam.BitVecConst.bvxor a).reprAux = toString "bvxor " ++ toString a ++ toString ""
- (Auto.Embedding.Lam.BitVecConst.bvnot a).reprAux = toString "bvnot " ++ toString a ++ toString ""
- (Auto.Embedding.Lam.BitVecConst.bvshOp a a_1 a_2).reprAux = Auto.Embedding.Lam.BVShOp.repr a a_1 a_2
- (Auto.Embedding.Lam.BitVecConst.bvappend a a_1).reprAux = toString "bvappend " ++ toString a ++ toString " " ++ toString a_1 ++ toString ""
- (Auto.Embedding.Lam.BitVecConst.bvextract a a_1 a_2).reprAux = toString "bvextract " ++ toString a ++ toString " " ++ toString a_1 ++ toString " " ++ toString a_2 ++ toString ""
- (Auto.Embedding.Lam.BitVecConst.bvrepeat a a_1).reprAux = toString "bvrepeat " ++ toString a ++ toString " " ++ toString a_1 ++ toString ""
- (Auto.Embedding.Lam.BitVecConst.bvzeroExtend a a_1).reprAux = toString "bvzeroExtend " ++ toString a ++ toString " " ++ toString a_1 ++ toString ""
- (Auto.Embedding.Lam.BitVecConst.bvsignExtend a a_1).reprAux = toString "bvsignExtend " ++ toString a ++ toString " " ++ toString a_1 ++ toString ""
Instances For
Equations
- b.reprPrec 0 = Std.format "Auto.Embedding.Lam.BitVecConst." ++ Std.format b.reprAux ++ Std.format ""
- b.reprPrec n_2.succ = Std.format "(." ++ Std.format b.reprAux ++ Std.format ")"
Instances For
Equations
Equations
- (Auto.Embedding.Lam.BitVecConst.bvVal a a_1).toString = toString (repr (BitVec.ofNat a a_1))
- (Auto.Embedding.Lam.BitVecConst.bvofNat a).toString = toString "bvofNat " ++ toString a ++ toString ""
- (Auto.Embedding.Lam.BitVecConst.bvtoNat a).toString = toString "bvtoNat " ++ toString a ++ toString ""
- (Auto.Embedding.Lam.BitVecConst.bvofInt a).toString = toString "bvofInt " ++ toString a ++ toString ""
- (Auto.Embedding.Lam.BitVecConst.bvtoInt a).toString = toString "bvtoInt " ++ toString a ++ toString ""
- (Auto.Embedding.Lam.BitVecConst.bvmsb a).toString = toString "bvmsb " ++ toString a ++ toString ""
- (Auto.Embedding.Lam.BitVecConst.bvaOp a a_1).toString = a_1.toString
- (Auto.Embedding.Lam.BitVecConst.bvneg a).toString = toString "-"
- (Auto.Embedding.Lam.BitVecConst.bvabs a).toString = toString "bvabs"
- (Auto.Embedding.Lam.BitVecConst.bvcmp a a_1 a_2).toString = Auto.Embedding.Lam.BVCmp.toString a_1 a_2
- (Auto.Embedding.Lam.BitVecConst.bvand a).toString = toString "&&&"
- (Auto.Embedding.Lam.BitVecConst.bvor a).toString = toString "|||"
- (Auto.Embedding.Lam.BitVecConst.bvxor a).toString = toString "^^^"
- (Auto.Embedding.Lam.BitVecConst.bvnot a).toString = toString "!"
- (Auto.Embedding.Lam.BitVecConst.bvshOp a a_1 a_2).toString = Auto.Embedding.Lam.BVShOp.toString a_1 a_2
- (Auto.Embedding.Lam.BitVecConst.bvappend a a_1).toString = toString "++"
- (Auto.Embedding.Lam.BitVecConst.bvextract a a_1 a_2).toString = toString "bvextract " ++ toString a_1 ++ toString " " ++ toString a_2 ++ toString ""
- (Auto.Embedding.Lam.BitVecConst.bvrepeat a a_1).toString = toString "bvrepeat " ++ toString a_1 ++ toString ""
- (Auto.Embedding.Lam.BitVecConst.bvzeroExtend a a_1).toString = toString "bvzeroExtend " ++ toString a_1 ++ toString ""
- (Auto.Embedding.Lam.BitVecConst.bvsignExtend a a_1).toString = toString "bvsignExtend " ++ toString a_1 ++ toString ""
Instances For
Equations
- (Auto.Embedding.Lam.BitVecConst.bvVal n₁ i₁).beq (Auto.Embedding.Lam.BitVecConst.bvVal n₂ i₂) = (n₁.beq n₂ && i₁.beq i₂)
- (Auto.Embedding.Lam.BitVecConst.bvofNat n₁).beq (Auto.Embedding.Lam.BitVecConst.bvofNat n₂) = n₁.beq n₂
- (Auto.Embedding.Lam.BitVecConst.bvtoNat n₁).beq (Auto.Embedding.Lam.BitVecConst.bvtoNat n₂) = n₁.beq n₂
- (Auto.Embedding.Lam.BitVecConst.bvofInt n₁).beq (Auto.Embedding.Lam.BitVecConst.bvofInt n₂) = n₁.beq n₂
- (Auto.Embedding.Lam.BitVecConst.bvtoInt n₁).beq (Auto.Embedding.Lam.BitVecConst.bvtoInt n₂) = n₁.beq n₂
- (Auto.Embedding.Lam.BitVecConst.bvmsb n₁).beq (Auto.Embedding.Lam.BitVecConst.bvmsb n₂) = n₁.beq n₂
- (Auto.Embedding.Lam.BitVecConst.bvaOp n₁ op₁).beq (Auto.Embedding.Lam.BitVecConst.bvaOp n₂ op₂) = (n₁.beq n₂ && op₁.beq op₂)
- (Auto.Embedding.Lam.BitVecConst.bvneg n₁).beq (Auto.Embedding.Lam.BitVecConst.bvneg n₂) = n₁.beq n₂
- (Auto.Embedding.Lam.BitVecConst.bvabs n₁).beq (Auto.Embedding.Lam.BitVecConst.bvabs n₂) = n₁.beq n₂
- (Auto.Embedding.Lam.BitVecConst.bvcmp n₁ prop₁ op₁).beq (Auto.Embedding.Lam.BitVecConst.bvcmp n₂ prop₂ op₂) = (n₁.beq n₂ && prop₁ == prop₂ && op₁.beq op₂)
- (Auto.Embedding.Lam.BitVecConst.bvand n₁).beq (Auto.Embedding.Lam.BitVecConst.bvand n₂) = n₁.beq n₂
- (Auto.Embedding.Lam.BitVecConst.bvor n₁).beq (Auto.Embedding.Lam.BitVecConst.bvor n₂) = n₁.beq n₂
- (Auto.Embedding.Lam.BitVecConst.bvxor n₁).beq (Auto.Embedding.Lam.BitVecConst.bvxor n₂) = n₁.beq n₂
- (Auto.Embedding.Lam.BitVecConst.bvnot n₁).beq (Auto.Embedding.Lam.BitVecConst.bvnot n₂) = n₁.beq n₂
- (Auto.Embedding.Lam.BitVecConst.bvshOp n₁ s₁ op₁).beq (Auto.Embedding.Lam.BitVecConst.bvshOp n₂ s₂ op₂) = (n₁.beq n₂ && s₁ == s₂ && op₁.beq op₂)
- (Auto.Embedding.Lam.BitVecConst.bvappend n₁ m₁).beq (Auto.Embedding.Lam.BitVecConst.bvappend n₂ m₂) = (n₁.beq n₂ && m₁.beq m₂)
- (Auto.Embedding.Lam.BitVecConst.bvextract n₁ h₁ l₁).beq (Auto.Embedding.Lam.BitVecConst.bvextract n₂ h₂ l₂) = (n₁.beq n₂ && h₁.beq h₂ && l₁.beq l₂)
- (Auto.Embedding.Lam.BitVecConst.bvrepeat w₁ i₁).beq (Auto.Embedding.Lam.BitVecConst.bvrepeat w₂ i₂) = (w₁.beq w₂ && i₁.beq i₂)
- (Auto.Embedding.Lam.BitVecConst.bvzeroExtend w₁ v₁).beq (Auto.Embedding.Lam.BitVecConst.bvzeroExtend w₂ v₂) = (w₁.beq w₂ && v₁.beq v₂)
- (Auto.Embedding.Lam.BitVecConst.bvsignExtend w₁ v₁).beq (Auto.Embedding.Lam.BitVecConst.bvsignExtend w₂ v₂) = (w₁.beq w₂ && v₁.beq v₂)
- x✝¹.beq x✝ = false
Instances For
Equations
- ⋯ = ⋯
Instances For
Equations
- ⋯ = ⋯
Instances For
Equations
- One or more equations did not get rendered due to their size.
- (Auto.Embedding.Lam.BitVecConst.bvVal a a_1).lamCheck = Auto.Embedding.Lam.LamSort.base (Auto.Embedding.Lam.LamBaseSort.bv a)
Instances For
- ofBvVal (n i : Nat) : (bvVal n i).LamWF (LamSort.base (LamBaseSort.bv n))
- ofBvofNat (n : Nat) : (bvofNat n).LamWF ((LamSort.base LamBaseSort.nat).func (LamSort.base (LamBaseSort.bv n)))
- ofBvtoNat (n : Nat) : (bvtoNat n).LamWF ((LamSort.base (LamBaseSort.bv n)).func (LamSort.base LamBaseSort.nat))
- ofBvofInt (n : Nat) : (bvofInt n).LamWF ((LamSort.base LamBaseSort.int).func (LamSort.base (LamBaseSort.bv n)))
- ofBvtoInt (n : Nat) : (bvtoInt n).LamWF ((LamSort.base (LamBaseSort.bv n)).func (LamSort.base LamBaseSort.int))
- ofBvmsb (n : Nat) : (bvmsb n).LamWF ((LamSort.base (LamBaseSort.bv n)).func (LamSort.base LamBaseSort.bool))
- ofBvaOp (n : Nat) (op : BVAOp) : (bvaOp n op).LamWF ((LamSort.base (LamBaseSort.bv n)).func ((LamSort.base (LamBaseSort.bv n)).func (LamSort.base (LamBaseSort.bv n))))
- ofBvneg (n : Nat) : (bvneg n).LamWF ((LamSort.base (LamBaseSort.bv n)).func (LamSort.base (LamBaseSort.bv n)))
- ofBvabs (n : Nat) : (bvabs n).LamWF ((LamSort.base (LamBaseSort.bv n)).func (LamSort.base (LamBaseSort.bv n)))
- ofBvcmp (n : Nat) (op : BVCmp) : (bvcmp n false op).LamWF ((LamSort.base (LamBaseSort.bv n)).func ((LamSort.base (LamBaseSort.bv n)).func (LamSort.base LamBaseSort.bool)))
- ofBvpropcmp (n : Nat) (op : BVCmp) : (bvcmp n true op).LamWF ((LamSort.base (LamBaseSort.bv n)).func ((LamSort.base (LamBaseSort.bv n)).func (LamSort.base LamBaseSort.prop)))
- ofBvand (n : Nat) : (bvand n).LamWF ((LamSort.base (LamBaseSort.bv n)).func ((LamSort.base (LamBaseSort.bv n)).func (LamSort.base (LamBaseSort.bv n))))
- ofBvor (n : Nat) : (bvor n).LamWF ((LamSort.base (LamBaseSort.bv n)).func ((LamSort.base (LamBaseSort.bv n)).func (LamSort.base (LamBaseSort.bv n))))
- ofBvxor (n : Nat) : (bvxor n).LamWF ((LamSort.base (LamBaseSort.bv n)).func ((LamSort.base (LamBaseSort.bv n)).func (LamSort.base (LamBaseSort.bv n))))
- ofBvnot (n : Nat) : (bvnot n).LamWF ((LamSort.base (LamBaseSort.bv n)).func (LamSort.base (LamBaseSort.bv n)))
- ofBvshOp (n : Nat) (op : BVShOp) : (bvshOp n false op).LamWF ((LamSort.base (LamBaseSort.bv n)).func ((LamSort.base LamBaseSort.nat).func (LamSort.base (LamBaseSort.bv n))))
- ofBvsmtshOp (n : Nat) (op : BVShOp) : (bvshOp n true op).LamWF ((LamSort.base (LamBaseSort.bv n)).func ((LamSort.base (LamBaseSort.bv n)).func (LamSort.base (LamBaseSort.bv n))))
- ofBvappend (n m : Nat) : (bvappend n m).LamWF ((LamSort.base (LamBaseSort.bv n)).func ((LamSort.base (LamBaseSort.bv m)).func (LamSort.base (LamBaseSort.bv (n.add m)))))
- ofBvextract (n h l : Nat) : (bvextract n h l).LamWF ((LamSort.base (LamBaseSort.bv n)).func (LamSort.base (LamBaseSort.bv ((h.sub l).add 1))))
- ofBvrepeat (w i : Nat) : (bvrepeat w i).LamWF ((LamSort.base (LamBaseSort.bv w)).func (LamSort.base (LamBaseSort.bv (w.mul i))))
- ofBvzeroExtend (w v : Nat) : (bvzeroExtend w v).LamWF ((LamSort.base (LamBaseSort.bv w)).func (LamSort.base (LamBaseSort.bv v)))
- ofBvsignExtend (w v : Nat) : (bvsignExtend w v).LamWF ((LamSort.base (LamBaseSort.bv w)).func (LamSort.base (LamBaseSort.bv v)))
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
- ⋯ = ⋯
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- ⋯ = ⋯
Instances For
Equations
- ⋯ = ⋯
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
- smtAttr1T : String → LamSort → LamSort → OtherConst
SMT attribute application, with one term as ⟨attribute_value⟩
.app _ (attribute ⟨keyword⟩ ⟨attr_term⟩) ⟨term⟩ ⇔ ⟨term⟩ ⟨keyword⟩ (⟨attr_term⟩)
smtAttr1T n s₁ s₂
is interpreted asfun (_ : s₁) (x₂ : s₂) => x₂
, which we'll denote asconstId
. Note that the interpretation is polymorphic. However, it does not need special treatment like∀, ∃, =
. This is becauseconstId A↑ B↑ = (constId A B)↑
, where↑
stands for universe level lifting.
Instances For
Equations
- Auto.Embedding.Lam.instToExprOtherConst = { toExpr := Auto.Embedding.Lam.toExprOtherConst✝, toTypeExpr := Lean.Expr.const `Auto.Embedding.Lam.OtherConst [] }
Equations
- p.reprPrec 0 = Std.format "Auto.Embedding.Lam.OtherConst." ++ Std.format p.reprAux ++ Std.format ""
- p.reprPrec n_2.succ = Std.format "(." ++ Std.format p.reprAux ++ Std.format ")"
Instances For
Equations
Equations
- Auto.Embedding.Lam.OtherConst.LamWF.ofOtherConst (Auto.Embedding.Lam.OtherConst.smtAttr1T a a_1 a_2) = ⟨a_1.func (a_2.func a_2), Auto.Embedding.Lam.OtherConst.LamWF.ofSmtAttr1T a a_1 a_2⟩
Instances For
Equations
Instances For
Equations
Instances For
Equations
Equations
- (Auto.Embedding.Lam.OtherConst.smtAttr1T n₁ sattr₁ sterm₁).beq (Auto.Embedding.Lam.OtherConst.smtAttr1T n₂ sattr₂ sterm₂) = (n₁ == n₂ && sattr₁.beq sattr₂ && sterm₁.beq sterm₂)
Instances For
Equations
Equations
- ⋯ = ⋯
Instances For
Equations
- ⋯ = ⋯
Instances For
Equations
- (Auto.Embedding.Lam.OtherConst.smtAttr1T a a_1 a_2).lamCheck = a_1.func (a_2.func a_2)
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- ⋯ = ⋯
Instances For
Equations
- ⋯ = ⋯
Instances For
Equations
- ⋯ = ⋯
Instances For
Equations
- ⋯ = ⋯
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Interpreted constants
Note that eq
, forallE
, existE
have ilVal/lamILTy
associated with them. During proof reconstruction, we should collect
the sort arguments of all eq, forallE, existE
that occurs in the
proof into ilVal
.
For ilVal
, we need to use ILLift.ofIsomTy
to construct
ILLift
structures. The idea is that we want the interpretation
of reified assumptions to be definitionally
equal to the assumption (or GLift.up
applied to the assumption, to
be precise), so we'll have to use the specially designed
of(Eq/Forall/Exist)Lift
function.
Note that at the end of the proof, we'll have a LamTerm.base .falseE
,
no =, ∀, ∃
left, so whatever (Eq/Forall/Exist)Lift
structure are within the (eq/forall/lam)Val
, the final result
will always interpret to GLift.up False
.
- pcst : PropConst → LamBaseTerm
- bcst : BoolConst → LamBaseTerm
- ncst : NatConst → LamBaseTerm
- icst : IntConst → LamBaseTerm
- scst : StringConst → LamBaseTerm
- bvcst : BitVecConst → LamBaseTerm
- ocst : OtherConst → LamBaseTerm
- eqI : Nat → LamBaseTerm
- forallEI : Nat → LamBaseTerm
- existEI : Nat → LamBaseTerm
- iteI : Nat → LamBaseTerm
- eq : LamSort → LamBaseTerm
- forallE : LamSort → LamBaseTerm
- existE : LamSort → LamBaseTerm
- ite : LamSort → LamBaseTerm
Instances For
Equations
- Auto.Embedding.Lam.instToExprLamBaseTerm = { toExpr := Auto.Embedding.Lam.toExprLamBaseTerm✝, toTypeExpr := Lean.Expr.const `Auto.Embedding.Lam.LamBaseTerm [] }
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Equations
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Equations
- (Auto.Embedding.Lam.LamBaseTerm.pcst a).toString = toString "" ++ toString a ++ toString ""
- (Auto.Embedding.Lam.LamBaseTerm.bcst a).toString = toString "" ++ toString a ++ toString ""
- (Auto.Embedding.Lam.LamBaseTerm.ncst a).toString = toString "" ++ toString a ++ toString ""
- (Auto.Embedding.Lam.LamBaseTerm.icst a).toString = toString "" ++ toString a ++ toString ""
- (Auto.Embedding.Lam.LamBaseTerm.scst a).toString = toString "" ++ toString a ++ toString ""
- (Auto.Embedding.Lam.LamBaseTerm.bvcst a).toString = toString "" ++ toString a ++ toString ""
- (Auto.Embedding.Lam.LamBaseTerm.ocst a).toString = toString "" ++ toString a ++ toString ""
- (Auto.Embedding.Lam.LamBaseTerm.eqI a).toString = "="
- (Auto.Embedding.Lam.LamBaseTerm.forallEI a).toString = "∀"
- (Auto.Embedding.Lam.LamBaseTerm.existEI a).toString = "∃"
- (Auto.Embedding.Lam.LamBaseTerm.iteI a).toString = "ite"
- (Auto.Embedding.Lam.LamBaseTerm.eq a).toString = "="
- (Auto.Embedding.Lam.LamBaseTerm.forallE a).toString = "∀"
- (Auto.Embedding.Lam.LamBaseTerm.existE a).toString = "∃"
- (Auto.Embedding.Lam.LamBaseTerm.ite a).toString = "ite"
Instances For
Equations
- (Auto.Embedding.Lam.LamBaseTerm.pcst pc₁).beq (Auto.Embedding.Lam.LamBaseTerm.pcst pc₂) = pc₁.beq pc₂
- (Auto.Embedding.Lam.LamBaseTerm.bcst bc₁).beq (Auto.Embedding.Lam.LamBaseTerm.bcst bc₂) = bc₁.beq bc₂
- (Auto.Embedding.Lam.LamBaseTerm.ncst nc₁).beq (Auto.Embedding.Lam.LamBaseTerm.ncst nc₂) = nc₁.beq nc₂
- (Auto.Embedding.Lam.LamBaseTerm.icst ic₁).beq (Auto.Embedding.Lam.LamBaseTerm.icst ic₂) = ic₁.beq ic₂
- (Auto.Embedding.Lam.LamBaseTerm.scst sc₁).beq (Auto.Embedding.Lam.LamBaseTerm.scst sc₂) = sc₁.beq sc₂
- (Auto.Embedding.Lam.LamBaseTerm.bvcst l₁).beq (Auto.Embedding.Lam.LamBaseTerm.bvcst l₂) = l₁.beq l₂
- (Auto.Embedding.Lam.LamBaseTerm.ocst o₁).beq (Auto.Embedding.Lam.LamBaseTerm.ocst o₂) = o₁.beq o₂
- (Auto.Embedding.Lam.LamBaseTerm.eqI n₁).beq (Auto.Embedding.Lam.LamBaseTerm.eqI n₂) = n₁.beq n₂
- (Auto.Embedding.Lam.LamBaseTerm.forallEI n₁).beq (Auto.Embedding.Lam.LamBaseTerm.forallEI n₂) = n₁.beq n₂
- (Auto.Embedding.Lam.LamBaseTerm.existEI n₁).beq (Auto.Embedding.Lam.LamBaseTerm.existEI n₂) = n₁.beq n₂
- (Auto.Embedding.Lam.LamBaseTerm.iteI n₁).beq (Auto.Embedding.Lam.LamBaseTerm.iteI n₂) = n₁.beq n₂
- (Auto.Embedding.Lam.LamBaseTerm.eq s₁).beq (Auto.Embedding.Lam.LamBaseTerm.eq s₂) = s₁.beq s₂
- (Auto.Embedding.Lam.LamBaseTerm.forallE s₁).beq (Auto.Embedding.Lam.LamBaseTerm.forallE s₂) = s₁.beq s₂
- (Auto.Embedding.Lam.LamBaseTerm.existE s₁).beq (Auto.Embedding.Lam.LamBaseTerm.existE s₂) = s₁.beq s₂
- (Auto.Embedding.Lam.LamBaseTerm.ite s₁).beq (Auto.Embedding.Lam.LamBaseTerm.ite s₂) = s₁.beq s₂
- x✝¹.beq x✝ = false
Instances For
Equations
- ⋯ = ⋯
Instances For
Equations
- ⋯ = ⋯
Instances For
Equations
- (Auto.Embedding.Lam.LamBaseTerm.pcst a).containsSort s = false
- (Auto.Embedding.Lam.LamBaseTerm.bcst a).containsSort s = false
- (Auto.Embedding.Lam.LamBaseTerm.ncst a).containsSort s = false
- (Auto.Embedding.Lam.LamBaseTerm.icst a).containsSort s = false
- (Auto.Embedding.Lam.LamBaseTerm.scst a).containsSort s = false
- (Auto.Embedding.Lam.LamBaseTerm.bvcst a).containsSort s = false
- (Auto.Embedding.Lam.LamBaseTerm.ocst a).containsSort s = false
- (Auto.Embedding.Lam.LamBaseTerm.eqI a).containsSort s = false
- (Auto.Embedding.Lam.LamBaseTerm.forallEI a).containsSort s = false
- (Auto.Embedding.Lam.LamBaseTerm.existEI a).containsSort s = false
- (Auto.Embedding.Lam.LamBaseTerm.iteI a).containsSort s = false
- (Auto.Embedding.Lam.LamBaseTerm.eq a).containsSort s = a.contains s
- (Auto.Embedding.Lam.LamBaseTerm.forallE a).containsSort s = a.contains s
- (Auto.Embedding.Lam.LamBaseTerm.existE a).containsSort s = a.contains s
- (Auto.Embedding.Lam.LamBaseTerm.ite a).containsSort s = a.contains s
Instances For
Equations
- Auto.Embedding.Lam.instInhabitedLamTyVal = { default := let func := fun (x : Nat) => Auto.Embedding.Lam.LamSort.atom 0; { lamVarTy := func, lamILTy := func, lamEVarTy := func } }
Equations
- One or more equations did not get rendered due to their size.
- Auto.Embedding.Lam.LamBaseTerm.lamCheck ltv (Auto.Embedding.Lam.LamBaseTerm.pcst a) = a.lamCheck
- Auto.Embedding.Lam.LamBaseTerm.lamCheck ltv (Auto.Embedding.Lam.LamBaseTerm.bcst a) = a.lamCheck
- Auto.Embedding.Lam.LamBaseTerm.lamCheck ltv (Auto.Embedding.Lam.LamBaseTerm.ncst a) = a.lamCheck
- Auto.Embedding.Lam.LamBaseTerm.lamCheck ltv (Auto.Embedding.Lam.LamBaseTerm.icst a) = a.lamCheck
- Auto.Embedding.Lam.LamBaseTerm.lamCheck ltv (Auto.Embedding.Lam.LamBaseTerm.scst a) = a.lamCheck
- Auto.Embedding.Lam.LamBaseTerm.lamCheck ltv (Auto.Embedding.Lam.LamBaseTerm.bvcst a) = a.lamCheck
- Auto.Embedding.Lam.LamBaseTerm.lamCheck ltv (Auto.Embedding.Lam.LamBaseTerm.ocst a) = a.lamCheck
- Auto.Embedding.Lam.LamBaseTerm.lamCheck ltv (Auto.Embedding.Lam.LamBaseTerm.eq a) = a.func (a.func (Auto.Embedding.Lam.LamSort.base Auto.Embedding.Lam.LamBaseSort.prop))
- Auto.Embedding.Lam.LamBaseTerm.lamCheck ltv (Auto.Embedding.Lam.LamBaseTerm.ite a) = (Auto.Embedding.Lam.LamSort.base Auto.Embedding.Lam.LamBaseSort.prop).func (a.func (a.func a))
Instances For
- ofPcst {ltv : LamTyVal} {pc : PropConst} {s : LamSort} (pcwf : pc.LamWF s) : LamWF ltv (pcst pc) s
- ofBcst {ltv : LamTyVal} {bc : BoolConst} {s : LamSort} (bcwf : bc.LamWF s) : LamWF ltv (bcst bc) s
- ofNcst {ltv : LamTyVal} {nc : NatConst} {s : LamSort} (ncwf : nc.LamWF s) : LamWF ltv (ncst nc) s
- ofIcst {ltv : LamTyVal} {ic : IntConst} {s : LamSort} (icwf : ic.LamWF s) : LamWF ltv (icst ic) s
- ofScst {ltv : LamTyVal} {sc : StringConst} {s : LamSort} (scwf : sc.LamWF s) : LamWF ltv (scst sc) s
- ofBvcst {ltv : LamTyVal} {bvc : BitVecConst} {s : LamSort} (bvcwf : bvc.LamWF s) : LamWF ltv (bvcst bvc) s
- ofOcst {ltv : LamTyVal} {oc : OtherConst} {s : LamSort} (ocwf : oc.LamWF s) : LamWF ltv (ocst oc) s
- ofEqI {ltv : LamTyVal} (n : Nat) : LamWF ltv (eqI n) ((ltv.lamILTy n).func ((ltv.lamILTy n).func (LamSort.base LamBaseSort.prop)))
- ofForallEI {ltv : LamTyVal} (n : Nat) : LamWF ltv (forallEI n) (((ltv.lamILTy n).func (LamSort.base LamBaseSort.prop)).func (LamSort.base LamBaseSort.prop))
- ofExistEI {ltv : LamTyVal} (n : Nat) : LamWF ltv (existEI n) (((ltv.lamILTy n).func (LamSort.base LamBaseSort.prop)).func (LamSort.base LamBaseSort.prop))
- ofIteI {ltv : LamTyVal} (n : Nat) : LamWF ltv (iteI n) ((LamSort.base LamBaseSort.prop).func ((ltv.lamILTy n).func ((ltv.lamILTy n).func (ltv.lamILTy n))))
- ofEq {ltv : LamTyVal} (s : LamSort) : LamWF ltv (eq s) (s.func (s.func (LamSort.base LamBaseSort.prop)))
- ofForallE {ltv : LamTyVal} (s : LamSort) : LamWF ltv (forallE s) ((s.func (LamSort.base LamBaseSort.prop)).func (LamSort.base LamBaseSort.prop))
- ofExistE {ltv : LamTyVal} (s : LamSort) : LamWF ltv (existE s) ((s.func (LamSort.base LamBaseSort.prop)).func (LamSort.base LamBaseSort.prop))
- ofIte {ltv : LamTyVal} (s : LamSort) : LamWF ltv (ite s) ((LamSort.base LamBaseSort.prop).func (s.func (s.func s)))
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
- (Auto.Embedding.Lam.LamBaseTerm.LamWF.ofScst scwf).getScst = scwf
Instances For
Equations
- (Auto.Embedding.Lam.LamBaseTerm.LamWF.ofBvcst bvcwf).getBvcst = bvcwf
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- ⋯ = ⋯
Instances For
Equations
- ⋯ = ⋯
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
- eqL : EqLift β
- forallL : ForallLift β
- existL : ExistLift β
- iteL : IteLift β
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
- varVal (n : Nat) : LamSort.interp self.tyVal (self.lamVarTy n)
- ilVal (n : Nat) : ILLift (LamSort.interp self.tyVal (self.lamILTy n))
- eVarVal (n : Nat) : LamSort.interp self.tyVal (self.lamEVarTy n)
Instances For
Equations
- Auto.Embedding.Lam.PropConst.interp tyVal Auto.Embedding.Lam.PropConst.trueE = { down := True }
- Auto.Embedding.Lam.PropConst.interp tyVal Auto.Embedding.Lam.PropConst.falseE = { down := False }
- Auto.Embedding.Lam.PropConst.interp tyVal Auto.Embedding.Lam.PropConst.not = Auto.Embedding.notLift
- Auto.Embedding.Lam.PropConst.interp tyVal Auto.Embedding.Lam.PropConst.and = Auto.Embedding.andLift
- Auto.Embedding.Lam.PropConst.interp tyVal Auto.Embedding.Lam.PropConst.or = Auto.Embedding.orLift
- Auto.Embedding.Lam.PropConst.interp tyVal Auto.Embedding.Lam.PropConst.imp = Auto.Embedding.impLift
- Auto.Embedding.Lam.PropConst.interp tyVal Auto.Embedding.Lam.PropConst.iff = Auto.Embedding.iffLift
Instances For
Equations
- Auto.Embedding.Lam.PropConst.LamWF.interp tyVal Auto.Embedding.Lam.PropConst.LamWF.ofTrueE = { down := True }
- Auto.Embedding.Lam.PropConst.LamWF.interp tyVal Auto.Embedding.Lam.PropConst.LamWF.ofFalseE = { down := False }
- Auto.Embedding.Lam.PropConst.LamWF.interp tyVal Auto.Embedding.Lam.PropConst.LamWF.ofNot = Auto.Embedding.notLift
- Auto.Embedding.Lam.PropConst.LamWF.interp tyVal Auto.Embedding.Lam.PropConst.LamWF.ofAnd = Auto.Embedding.andLift
- Auto.Embedding.Lam.PropConst.LamWF.interp tyVal Auto.Embedding.Lam.PropConst.LamWF.ofOr = Auto.Embedding.orLift
- Auto.Embedding.Lam.PropConst.LamWF.interp tyVal Auto.Embedding.Lam.PropConst.LamWF.ofImp = Auto.Embedding.impLift
- Auto.Embedding.Lam.PropConst.LamWF.interp tyVal Auto.Embedding.Lam.PropConst.LamWF.ofIff = Auto.Embedding.iffLift
Instances For
Equations
- Auto.Embedding.Lam.BoolConst.interp tyVal Auto.Embedding.Lam.BoolConst.ofProp = Auto.Embedding.ofPropLift
- Auto.Embedding.Lam.BoolConst.interp tyVal Auto.Embedding.Lam.BoolConst.trueb = { down := true }
- Auto.Embedding.Lam.BoolConst.interp tyVal Auto.Embedding.Lam.BoolConst.falseb = { down := false }
- Auto.Embedding.Lam.BoolConst.interp tyVal Auto.Embedding.Lam.BoolConst.notb = Auto.Embedding.notbLift
- Auto.Embedding.Lam.BoolConst.interp tyVal Auto.Embedding.Lam.BoolConst.andb = Auto.Embedding.andbLift
- Auto.Embedding.Lam.BoolConst.interp tyVal Auto.Embedding.Lam.BoolConst.orb = Auto.Embedding.orbLift
Instances For
Equations
- Auto.Embedding.Lam.BoolConst.LamWF.interp tyVal Auto.Embedding.Lam.BoolConst.LamWF.ofOfProp = Auto.Embedding.ofPropLift
- Auto.Embedding.Lam.BoolConst.LamWF.interp tyVal Auto.Embedding.Lam.BoolConst.LamWF.ofTrueB = { down := true }
- Auto.Embedding.Lam.BoolConst.LamWF.interp tyVal Auto.Embedding.Lam.BoolConst.LamWF.ofFalseB = { down := false }
- Auto.Embedding.Lam.BoolConst.LamWF.interp tyVal Auto.Embedding.Lam.BoolConst.LamWF.ofNotB = Auto.Embedding.notbLift
- Auto.Embedding.Lam.BoolConst.LamWF.interp tyVal Auto.Embedding.Lam.BoolConst.LamWF.ofAndB = Auto.Embedding.andbLift
- Auto.Embedding.Lam.BoolConst.LamWF.interp tyVal Auto.Embedding.Lam.BoolConst.LamWF.ofOrB = Auto.Embedding.orbLift
Instances For
Equations
- Auto.Embedding.Lam.NatConst.interp tyVal (Auto.Embedding.Lam.NatConst.natVal a) = { down := a }
- Auto.Embedding.Lam.NatConst.interp tyVal Auto.Embedding.Lam.NatConst.nadd = Auto.Embedding.naddLift
- Auto.Embedding.Lam.NatConst.interp tyVal Auto.Embedding.Lam.NatConst.nsub = Auto.Embedding.nsubLift
- Auto.Embedding.Lam.NatConst.interp tyVal Auto.Embedding.Lam.NatConst.nmul = Auto.Embedding.nmulLift
- Auto.Embedding.Lam.NatConst.interp tyVal Auto.Embedding.Lam.NatConst.ndiv = Auto.Embedding.ndivLift
- Auto.Embedding.Lam.NatConst.interp tyVal Auto.Embedding.Lam.NatConst.nmod = Auto.Embedding.nmodLift
- Auto.Embedding.Lam.NatConst.interp tyVal Auto.Embedding.Lam.NatConst.nle = Auto.Embedding.nleLift
- Auto.Embedding.Lam.NatConst.interp tyVal Auto.Embedding.Lam.NatConst.nlt = Auto.Embedding.nltLift
- Auto.Embedding.Lam.NatConst.interp tyVal Auto.Embedding.Lam.NatConst.nmax = Auto.Embedding.nmaxLift
- Auto.Embedding.Lam.NatConst.interp tyVal Auto.Embedding.Lam.NatConst.nmin = Auto.Embedding.nminLift
Instances For
Equations
- Auto.Embedding.Lam.NatConst.LamWF.interp tyVal (Auto.Embedding.Lam.NatConst.LamWF.ofNatVal n) = { down := n }
- Auto.Embedding.Lam.NatConst.LamWF.interp tyVal Auto.Embedding.Lam.NatConst.LamWF.ofNadd = Auto.Embedding.naddLift
- Auto.Embedding.Lam.NatConst.LamWF.interp tyVal Auto.Embedding.Lam.NatConst.LamWF.ofNsub = Auto.Embedding.nsubLift
- Auto.Embedding.Lam.NatConst.LamWF.interp tyVal Auto.Embedding.Lam.NatConst.LamWF.ofNmul = Auto.Embedding.nmulLift
- Auto.Embedding.Lam.NatConst.LamWF.interp tyVal Auto.Embedding.Lam.NatConst.LamWF.ofNdiv = Auto.Embedding.ndivLift
- Auto.Embedding.Lam.NatConst.LamWF.interp tyVal Auto.Embedding.Lam.NatConst.LamWF.ofNmod = Auto.Embedding.nmodLift
- Auto.Embedding.Lam.NatConst.LamWF.interp tyVal Auto.Embedding.Lam.NatConst.LamWF.ofNle = Auto.Embedding.nleLift
- Auto.Embedding.Lam.NatConst.LamWF.interp tyVal Auto.Embedding.Lam.NatConst.LamWF.ofNlt = Auto.Embedding.nltLift
- Auto.Embedding.Lam.NatConst.LamWF.interp tyVal Auto.Embedding.Lam.NatConst.LamWF.ofNmax = Auto.Embedding.nmaxLift
- Auto.Embedding.Lam.NatConst.LamWF.interp tyVal Auto.Embedding.Lam.NatConst.LamWF.ofNmin = Auto.Embedding.nminLift
Instances For
Equations
- Auto.Embedding.Lam.IntConst.interp tyVal Auto.Embedding.Lam.IntConst.iofNat = Auto.Embedding.iofNatLift
- Auto.Embedding.Lam.IntConst.interp tyVal Auto.Embedding.Lam.IntConst.inegSucc = Auto.Embedding.inegSuccLift
- Auto.Embedding.Lam.IntConst.interp tyVal Auto.Embedding.Lam.IntConst.ineg = Auto.Embedding.inegLift
- Auto.Embedding.Lam.IntConst.interp tyVal Auto.Embedding.Lam.IntConst.iabs = Auto.Embedding.iabsLift
- Auto.Embedding.Lam.IntConst.interp tyVal Auto.Embedding.Lam.IntConst.iadd = Auto.Embedding.iaddLift
- Auto.Embedding.Lam.IntConst.interp tyVal Auto.Embedding.Lam.IntConst.isub = Auto.Embedding.isubLift
- Auto.Embedding.Lam.IntConst.interp tyVal Auto.Embedding.Lam.IntConst.imul = Auto.Embedding.imulLift
- Auto.Embedding.Lam.IntConst.interp tyVal Auto.Embedding.Lam.IntConst.idiv = Auto.Embedding.idivLift
- Auto.Embedding.Lam.IntConst.interp tyVal Auto.Embedding.Lam.IntConst.imod = Auto.Embedding.imodLift
- Auto.Embedding.Lam.IntConst.interp tyVal Auto.Embedding.Lam.IntConst.iediv = Auto.Embedding.iedivLift
- Auto.Embedding.Lam.IntConst.interp tyVal Auto.Embedding.Lam.IntConst.iemod = Auto.Embedding.iemodLift
- Auto.Embedding.Lam.IntConst.interp tyVal Auto.Embedding.Lam.IntConst.ile = Auto.Embedding.ileLift
- Auto.Embedding.Lam.IntConst.interp tyVal Auto.Embedding.Lam.IntConst.ilt = Auto.Embedding.iltLift
- Auto.Embedding.Lam.IntConst.interp tyVal Auto.Embedding.Lam.IntConst.imax = Auto.Embedding.imaxLift
- Auto.Embedding.Lam.IntConst.interp tyVal Auto.Embedding.Lam.IntConst.imin = Auto.Embedding.iminLift
Instances For
Equations
- Auto.Embedding.Lam.IntConst.LamWF.interp tyVal Auto.Embedding.Lam.IntConst.LamWF.ofIOfNat = Auto.Embedding.iofNatLift
- Auto.Embedding.Lam.IntConst.LamWF.interp tyVal Auto.Embedding.Lam.IntConst.LamWF.ofINegSucc = Auto.Embedding.inegSuccLift
- Auto.Embedding.Lam.IntConst.LamWF.interp tyVal Auto.Embedding.Lam.IntConst.LamWF.ofIneg = Auto.Embedding.inegLift
- Auto.Embedding.Lam.IntConst.LamWF.interp tyVal Auto.Embedding.Lam.IntConst.LamWF.ofIabs = Auto.Embedding.iabsLift
- Auto.Embedding.Lam.IntConst.LamWF.interp tyVal Auto.Embedding.Lam.IntConst.LamWF.ofIadd = Auto.Embedding.iaddLift
- Auto.Embedding.Lam.IntConst.LamWF.interp tyVal Auto.Embedding.Lam.IntConst.LamWF.ofIsub = Auto.Embedding.isubLift
- Auto.Embedding.Lam.IntConst.LamWF.interp tyVal Auto.Embedding.Lam.IntConst.LamWF.ofImul = Auto.Embedding.imulLift
- Auto.Embedding.Lam.IntConst.LamWF.interp tyVal Auto.Embedding.Lam.IntConst.LamWF.ofIdiv = Auto.Embedding.idivLift
- Auto.Embedding.Lam.IntConst.LamWF.interp tyVal Auto.Embedding.Lam.IntConst.LamWF.ofImod = Auto.Embedding.imodLift
- Auto.Embedding.Lam.IntConst.LamWF.interp tyVal Auto.Embedding.Lam.IntConst.LamWF.ofIediv = Auto.Embedding.iedivLift
- Auto.Embedding.Lam.IntConst.LamWF.interp tyVal Auto.Embedding.Lam.IntConst.LamWF.ofIemod = Auto.Embedding.iemodLift
- Auto.Embedding.Lam.IntConst.LamWF.interp tyVal Auto.Embedding.Lam.IntConst.LamWF.ofIle = Auto.Embedding.ileLift
- Auto.Embedding.Lam.IntConst.LamWF.interp tyVal Auto.Embedding.Lam.IntConst.LamWF.ofIlt = Auto.Embedding.iltLift
- Auto.Embedding.Lam.IntConst.LamWF.interp tyVal Auto.Embedding.Lam.IntConst.LamWF.ofImax = Auto.Embedding.imaxLift
- Auto.Embedding.Lam.IntConst.LamWF.interp tyVal Auto.Embedding.Lam.IntConst.LamWF.ofImin = Auto.Embedding.iminLift
Instances For
Equations
- Auto.Embedding.Lam.StringConst.interp tyVal (Auto.Embedding.Lam.StringConst.strVal a) = { down := a }
- Auto.Embedding.Lam.StringConst.interp tyVal Auto.Embedding.Lam.StringConst.slength = Auto.Embedding.slengthLift
- Auto.Embedding.Lam.StringConst.interp tyVal Auto.Embedding.Lam.StringConst.sapp = Auto.Embedding.sappLift
- Auto.Embedding.Lam.StringConst.interp tyVal Auto.Embedding.Lam.StringConst.sle = Auto.Embedding.sleLift
- Auto.Embedding.Lam.StringConst.interp tyVal Auto.Embedding.Lam.StringConst.slt = Auto.Embedding.sltLift
- Auto.Embedding.Lam.StringConst.interp tyVal Auto.Embedding.Lam.StringConst.sprefixof = Auto.Embedding.sprefixofLift
- Auto.Embedding.Lam.StringConst.interp tyVal Auto.Embedding.Lam.StringConst.srepall = Auto.Embedding.srepallLift
Instances For
Equations
- Auto.Embedding.Lam.StringConst.LamWF.interp tyVal (Auto.Embedding.Lam.StringConst.LamWF.ofStrVal s_2) = { down := s_2 }
- Auto.Embedding.Lam.StringConst.LamWF.interp tyVal Auto.Embedding.Lam.StringConst.LamWF.ofSlength = Auto.Embedding.slengthLift
- Auto.Embedding.Lam.StringConst.LamWF.interp tyVal Auto.Embedding.Lam.StringConst.LamWF.ofSapp = Auto.Embedding.sappLift
- Auto.Embedding.Lam.StringConst.LamWF.interp tyVal Auto.Embedding.Lam.StringConst.LamWF.ofSle = Auto.Embedding.sleLift
- Auto.Embedding.Lam.StringConst.LamWF.interp tyVal Auto.Embedding.Lam.StringConst.LamWF.ofSlt = Auto.Embedding.sltLift
- Auto.Embedding.Lam.StringConst.LamWF.interp tyVal Auto.Embedding.Lam.StringConst.LamWF.ofSprefixof = Auto.Embedding.sprefixofLift
- Auto.Embedding.Lam.StringConst.LamWF.interp tyVal Auto.Embedding.Lam.StringConst.LamWF.ofSrepall = Auto.Embedding.srepallLift
Instances For
Equations
- ⋯ = ⋯
Instances For
Equations
- Auto.Embedding.Lam.BVAOp.interp n Auto.Embedding.Lam.BVAOp.add = Auto.Embedding.bvaddLift n
- Auto.Embedding.Lam.BVAOp.interp n Auto.Embedding.Lam.BVAOp.sub = Auto.Embedding.bvsubLift n
- Auto.Embedding.Lam.BVAOp.interp n Auto.Embedding.Lam.BVAOp.mul = Auto.Embedding.bvmulLift n
- Auto.Embedding.Lam.BVAOp.interp n Auto.Embedding.Lam.BVAOp.udiv = Auto.Embedding.bvudivLift n
- Auto.Embedding.Lam.BVAOp.interp n Auto.Embedding.Lam.BVAOp.urem = Auto.Embedding.bvuremLift n
- Auto.Embedding.Lam.BVAOp.interp n Auto.Embedding.Lam.BVAOp.sdiv = Auto.Embedding.bvsdivLift n
- Auto.Embedding.Lam.BVAOp.interp n Auto.Embedding.Lam.BVAOp.srem = Auto.Embedding.bvsremLift n
- Auto.Embedding.Lam.BVAOp.interp n Auto.Embedding.Lam.BVAOp.smod = Auto.Embedding.bvsmodLift n
Instances For
Equations
- Auto.Embedding.Lam.BVCmp.interp n Auto.Embedding.Lam.BVCmp.ult = Auto.Embedding.bvultLift n
- Auto.Embedding.Lam.BVCmp.interp n Auto.Embedding.Lam.BVCmp.ule = Auto.Embedding.bvuleLift n
- Auto.Embedding.Lam.BVCmp.interp n Auto.Embedding.Lam.BVCmp.slt = Auto.Embedding.bvsltLift n
- Auto.Embedding.Lam.BVCmp.interp n Auto.Embedding.Lam.BVCmp.sle = Auto.Embedding.bvsleLift n
Instances For
Equations
- Auto.Embedding.Lam.BVCmp.propinterp n Auto.Embedding.Lam.BVCmp.ult = Auto.Embedding.bvpropultLift n
- Auto.Embedding.Lam.BVCmp.propinterp n Auto.Embedding.Lam.BVCmp.ule = Auto.Embedding.bvpropuleLift n
- Auto.Embedding.Lam.BVCmp.propinterp n Auto.Embedding.Lam.BVCmp.slt = Auto.Embedding.bvpropsltLift n
- Auto.Embedding.Lam.BVCmp.propinterp n Auto.Embedding.Lam.BVCmp.sle = Auto.Embedding.bvpropsleLift n
Instances For
Equations
- Auto.Embedding.Lam.BVShOp.smtinterp n Auto.Embedding.Lam.BVShOp.shl = Auto.Embedding.bvsmtshlLift n
- Auto.Embedding.Lam.BVShOp.smtinterp n Auto.Embedding.Lam.BVShOp.lshr = Auto.Embedding.bvsmtlshrLift n
- Auto.Embedding.Lam.BVShOp.smtinterp n Auto.Embedding.Lam.BVShOp.ashr = Auto.Embedding.bvsmtashrLift n
Instances For
Equations
- Auto.Embedding.Lam.BitVecConst.interp tyVal (Auto.Embedding.Lam.BitVecConst.bvVal n i) = { down := BitVec.ofNat n i }
- Auto.Embedding.Lam.BitVecConst.interp tyVal (Auto.Embedding.Lam.BitVecConst.bvofNat n) = Auto.Embedding.bvofNatLift n
- Auto.Embedding.Lam.BitVecConst.interp tyVal (Auto.Embedding.Lam.BitVecConst.bvtoNat n) = Auto.Embedding.bvtoNatLift n
- Auto.Embedding.Lam.BitVecConst.interp tyVal (Auto.Embedding.Lam.BitVecConst.bvofInt n) = Auto.Embedding.bvofIntLift n
- Auto.Embedding.Lam.BitVecConst.interp tyVal (Auto.Embedding.Lam.BitVecConst.bvtoInt n) = Auto.Embedding.bvtoIntLift n
- Auto.Embedding.Lam.BitVecConst.interp tyVal (Auto.Embedding.Lam.BitVecConst.bvmsb n) = Auto.Embedding.bvmsbLift n
- Auto.Embedding.Lam.BitVecConst.interp tyVal (Auto.Embedding.Lam.BitVecConst.bvaOp n op) = Auto.Embedding.Lam.BVAOp.interp n op
- Auto.Embedding.Lam.BitVecConst.interp tyVal (Auto.Embedding.Lam.BitVecConst.bvneg n) = Auto.Embedding.bvnegLift n
- Auto.Embedding.Lam.BitVecConst.interp tyVal (Auto.Embedding.Lam.BitVecConst.bvabs n) = Auto.Embedding.bvabsLift n
- Auto.Embedding.Lam.BitVecConst.interp tyVal (Auto.Embedding.Lam.BitVecConst.bvcmp n false op) = Auto.Embedding.Lam.BVCmp.interp n op
- Auto.Embedding.Lam.BitVecConst.interp tyVal (Auto.Embedding.Lam.BitVecConst.bvcmp n true op) = Auto.Embedding.Lam.BVCmp.propinterp n op
- Auto.Embedding.Lam.BitVecConst.interp tyVal (Auto.Embedding.Lam.BitVecConst.bvand n) = Auto.Embedding.bvandLift n
- Auto.Embedding.Lam.BitVecConst.interp tyVal (Auto.Embedding.Lam.BitVecConst.bvor n) = Auto.Embedding.bvorLift n
- Auto.Embedding.Lam.BitVecConst.interp tyVal (Auto.Embedding.Lam.BitVecConst.bvxor n) = Auto.Embedding.bvxorLift n
- Auto.Embedding.Lam.BitVecConst.interp tyVal (Auto.Embedding.Lam.BitVecConst.bvnot n) = Auto.Embedding.bvnotLift n
- Auto.Embedding.Lam.BitVecConst.interp tyVal (Auto.Embedding.Lam.BitVecConst.bvshOp n false op) = Auto.Embedding.Lam.BVShOp.interp n op
- Auto.Embedding.Lam.BitVecConst.interp tyVal (Auto.Embedding.Lam.BitVecConst.bvshOp n true op) = Auto.Embedding.Lam.BVShOp.smtinterp n op
- Auto.Embedding.Lam.BitVecConst.interp tyVal (Auto.Embedding.Lam.BitVecConst.bvappend n m) = Auto.Embedding.bvappendLift n m
- Auto.Embedding.Lam.BitVecConst.interp tyVal (Auto.Embedding.Lam.BitVecConst.bvextract n h l) = Auto.Embedding.bvextractLift n h l
- Auto.Embedding.Lam.BitVecConst.interp tyVal (Auto.Embedding.Lam.BitVecConst.bvrepeat w i) = Auto.Embedding.bvrepeatLift w i
- Auto.Embedding.Lam.BitVecConst.interp tyVal (Auto.Embedding.Lam.BitVecConst.bvzeroExtend w v) = Auto.Embedding.bvzeroExtendLift w v
- Auto.Embedding.Lam.BitVecConst.interp tyVal (Auto.Embedding.Lam.BitVecConst.bvsignExtend w v) = Auto.Embedding.bvsignExtendLift w v
Instances For
Equations
- Auto.Embedding.Lam.BitVecConst.LamWF.interp tyVal (Auto.Embedding.Lam.BitVecConst.LamWF.ofBvVal n i) = { down := BitVec.ofNat n i }
- Auto.Embedding.Lam.BitVecConst.LamWF.interp tyVal (Auto.Embedding.Lam.BitVecConst.LamWF.ofBvofNat n) = Auto.Embedding.bvofNatLift n
- Auto.Embedding.Lam.BitVecConst.LamWF.interp tyVal (Auto.Embedding.Lam.BitVecConst.LamWF.ofBvtoNat n) = Auto.Embedding.bvtoNatLift n
- Auto.Embedding.Lam.BitVecConst.LamWF.interp tyVal (Auto.Embedding.Lam.BitVecConst.LamWF.ofBvofInt n) = Auto.Embedding.bvofIntLift n
- Auto.Embedding.Lam.BitVecConst.LamWF.interp tyVal (Auto.Embedding.Lam.BitVecConst.LamWF.ofBvtoInt n) = Auto.Embedding.bvtoIntLift n
- Auto.Embedding.Lam.BitVecConst.LamWF.interp tyVal (Auto.Embedding.Lam.BitVecConst.LamWF.ofBvmsb n) = Auto.Embedding.bvmsbLift n
- Auto.Embedding.Lam.BitVecConst.LamWF.interp tyVal (Auto.Embedding.Lam.BitVecConst.LamWF.ofBvaOp n op) = Auto.Embedding.Lam.BVAOp.interp n op
- Auto.Embedding.Lam.BitVecConst.LamWF.interp tyVal (Auto.Embedding.Lam.BitVecConst.LamWF.ofBvneg n) = Auto.Embedding.bvnegLift n
- Auto.Embedding.Lam.BitVecConst.LamWF.interp tyVal (Auto.Embedding.Lam.BitVecConst.LamWF.ofBvabs n) = Auto.Embedding.bvabsLift n
- Auto.Embedding.Lam.BitVecConst.LamWF.interp tyVal (Auto.Embedding.Lam.BitVecConst.LamWF.ofBvcmp n op) = Auto.Embedding.Lam.BVCmp.interp n op
- Auto.Embedding.Lam.BitVecConst.LamWF.interp tyVal (Auto.Embedding.Lam.BitVecConst.LamWF.ofBvpropcmp n op) = Auto.Embedding.Lam.BVCmp.propinterp n op
- Auto.Embedding.Lam.BitVecConst.LamWF.interp tyVal (Auto.Embedding.Lam.BitVecConst.LamWF.ofBvand n) = Auto.Embedding.bvandLift n
- Auto.Embedding.Lam.BitVecConst.LamWF.interp tyVal (Auto.Embedding.Lam.BitVecConst.LamWF.ofBvor n) = Auto.Embedding.bvorLift n
- Auto.Embedding.Lam.BitVecConst.LamWF.interp tyVal (Auto.Embedding.Lam.BitVecConst.LamWF.ofBvxor n) = Auto.Embedding.bvxorLift n
- Auto.Embedding.Lam.BitVecConst.LamWF.interp tyVal (Auto.Embedding.Lam.BitVecConst.LamWF.ofBvnot n) = Auto.Embedding.bvnotLift n
- Auto.Embedding.Lam.BitVecConst.LamWF.interp tyVal (Auto.Embedding.Lam.BitVecConst.LamWF.ofBvshOp n op) = Auto.Embedding.Lam.BVShOp.interp n op
- Auto.Embedding.Lam.BitVecConst.LamWF.interp tyVal (Auto.Embedding.Lam.BitVecConst.LamWF.ofBvsmtshOp n op) = Auto.Embedding.Lam.BVShOp.smtinterp n op
- Auto.Embedding.Lam.BitVecConst.LamWF.interp tyVal (Auto.Embedding.Lam.BitVecConst.LamWF.ofBvappend n m) = Auto.Embedding.bvappendLift n m
- Auto.Embedding.Lam.BitVecConst.LamWF.interp tyVal (Auto.Embedding.Lam.BitVecConst.LamWF.ofBvextract n h l) = Auto.Embedding.bvextractLift n h l
- Auto.Embedding.Lam.BitVecConst.LamWF.interp tyVal (Auto.Embedding.Lam.BitVecConst.LamWF.ofBvrepeat w i) = Auto.Embedding.bvrepeatLift w i
- Auto.Embedding.Lam.BitVecConst.LamWF.interp tyVal (Auto.Embedding.Lam.BitVecConst.LamWF.ofBvzeroExtend w v) = Auto.Embedding.bvzeroExtendLift w v
- Auto.Embedding.Lam.BitVecConst.LamWF.interp tyVal (Auto.Embedding.Lam.BitVecConst.LamWF.ofBvsignExtend w v) = Auto.Embedding.bvsignExtendLift w v
Instances For
Equations
- ⋯ = ⋯
Instances For
Equations
- Auto.Embedding.Lam.LamBaseTerm.interp lval (Auto.Embedding.Lam.LamBaseTerm.pcst a) = Auto.Embedding.Lam.PropConst.interp lval.tyVal a
- Auto.Embedding.Lam.LamBaseTerm.interp lval (Auto.Embedding.Lam.LamBaseTerm.bcst a) = Auto.Embedding.Lam.BoolConst.interp lval.tyVal a
- Auto.Embedding.Lam.LamBaseTerm.interp lval (Auto.Embedding.Lam.LamBaseTerm.ncst a) = Auto.Embedding.Lam.NatConst.interp lval.tyVal a
- Auto.Embedding.Lam.LamBaseTerm.interp lval (Auto.Embedding.Lam.LamBaseTerm.icst a) = Auto.Embedding.Lam.IntConst.interp lval.tyVal a
- Auto.Embedding.Lam.LamBaseTerm.interp lval (Auto.Embedding.Lam.LamBaseTerm.scst a) = Auto.Embedding.Lam.StringConst.interp lval.tyVal a
- Auto.Embedding.Lam.LamBaseTerm.interp lval (Auto.Embedding.Lam.LamBaseTerm.bvcst a) = Auto.Embedding.Lam.BitVecConst.interp lval.tyVal a
- Auto.Embedding.Lam.LamBaseTerm.interp lval (Auto.Embedding.Lam.LamBaseTerm.ocst a) = Auto.Embedding.Lam.OtherConst.interp lval.tyVal a
- Auto.Embedding.Lam.LamBaseTerm.interp lval (Auto.Embedding.Lam.LamBaseTerm.eqI a) = (lval.ilVal a).eqL.eqF
- Auto.Embedding.Lam.LamBaseTerm.interp lval (Auto.Embedding.Lam.LamBaseTerm.forallEI a) = (lval.ilVal a).forallL.forallF
- Auto.Embedding.Lam.LamBaseTerm.interp lval (Auto.Embedding.Lam.LamBaseTerm.existEI a) = (lval.ilVal a).existL.existF
- Auto.Embedding.Lam.LamBaseTerm.interp lval (Auto.Embedding.Lam.LamBaseTerm.iteI a) = (lval.ilVal a).iteL.iteF
- Auto.Embedding.Lam.LamBaseTerm.interp lval (Auto.Embedding.Lam.LamBaseTerm.eq a) = Auto.Embedding.eqLiftFn (Auto.Embedding.Lam.LamSort.interp lval.tyVal a)
- Auto.Embedding.Lam.LamBaseTerm.interp lval (Auto.Embedding.Lam.LamBaseTerm.forallE a) = Auto.Embedding.forallLiftFn (Auto.Embedding.Lam.LamSort.interp lval.tyVal a)
- Auto.Embedding.Lam.LamBaseTerm.interp lval (Auto.Embedding.Lam.LamBaseTerm.existE a) = Auto.Embedding.existLiftFn (Auto.Embedding.Lam.LamSort.interp lval.tyVal a)
- Auto.Embedding.Lam.LamBaseTerm.interp lval (Auto.Embedding.Lam.LamBaseTerm.ite a) = Auto.Embedding.iteLiftFn (Auto.Embedding.Lam.LamSort.interp lval.tyVal a)
Instances For
Equations
- Auto.Embedding.Lam.LamBaseTerm.LamWF.interp lval (Auto.Embedding.Lam.LamBaseTerm.LamWF.ofPcst wf) = Auto.Embedding.Lam.PropConst.LamWF.interp lval.tyVal wf
- Auto.Embedding.Lam.LamBaseTerm.LamWF.interp lval (Auto.Embedding.Lam.LamBaseTerm.LamWF.ofBcst wf) = Auto.Embedding.Lam.BoolConst.LamWF.interp lval.tyVal wf
- Auto.Embedding.Lam.LamBaseTerm.LamWF.interp lval (Auto.Embedding.Lam.LamBaseTerm.LamWF.ofNcst wf) = Auto.Embedding.Lam.NatConst.LamWF.interp lval.tyVal wf
- Auto.Embedding.Lam.LamBaseTerm.LamWF.interp lval (Auto.Embedding.Lam.LamBaseTerm.LamWF.ofIcst wf) = Auto.Embedding.Lam.IntConst.LamWF.interp lval.tyVal wf
- Auto.Embedding.Lam.LamBaseTerm.LamWF.interp lval (Auto.Embedding.Lam.LamBaseTerm.LamWF.ofScst wf) = Auto.Embedding.Lam.StringConst.LamWF.interp lval.tyVal wf
- Auto.Embedding.Lam.LamBaseTerm.LamWF.interp lval (Auto.Embedding.Lam.LamBaseTerm.LamWF.ofBvcst wf) = Auto.Embedding.Lam.BitVecConst.LamWF.interp lval.tyVal wf
- Auto.Embedding.Lam.LamBaseTerm.LamWF.interp lval (Auto.Embedding.Lam.LamBaseTerm.LamWF.ofOcst wf) = Auto.Embedding.Lam.OtherConst.LamWF.interp lval.tyVal wf
- Auto.Embedding.Lam.LamBaseTerm.LamWF.interp lval (Auto.Embedding.Lam.LamBaseTerm.LamWF.ofEqI n) = (lval.ilVal n).eqL.eqF
- Auto.Embedding.Lam.LamBaseTerm.LamWF.interp lval (Auto.Embedding.Lam.LamBaseTerm.LamWF.ofForallEI n) = (lval.ilVal n).forallL.forallF
- Auto.Embedding.Lam.LamBaseTerm.LamWF.interp lval (Auto.Embedding.Lam.LamBaseTerm.LamWF.ofExistEI n) = (lval.ilVal n).existL.existF
- Auto.Embedding.Lam.LamBaseTerm.LamWF.interp lval (Auto.Embedding.Lam.LamBaseTerm.LamWF.ofIteI n) = (lval.ilVal n).iteL.iteF
- Auto.Embedding.Lam.LamBaseTerm.LamWF.interp lval (Auto.Embedding.Lam.LamBaseTerm.LamWF.ofEq s_2) = Auto.Embedding.eqLiftFn (Auto.Embedding.Lam.LamSort.interp lval.tyVal s_2)
- Auto.Embedding.Lam.LamBaseTerm.LamWF.interp lval (Auto.Embedding.Lam.LamBaseTerm.LamWF.ofForallE s_2) = Auto.Embedding.forallLiftFn (Auto.Embedding.Lam.LamSort.interp lval.tyVal s_2)
- Auto.Embedding.Lam.LamBaseTerm.LamWF.interp lval (Auto.Embedding.Lam.LamBaseTerm.LamWF.ofExistE s_2) = Auto.Embedding.existLiftFn (Auto.Embedding.Lam.LamSort.interp lval.tyVal s_2)
- Auto.Embedding.Lam.LamBaseTerm.LamWF.interp lval (Auto.Embedding.Lam.LamBaseTerm.LamWF.ofIte s_2) = Auto.Embedding.iteLiftFn (Auto.Embedding.Lam.LamSort.interp lval.tyVal s_2)
Instances For
Equations
- ⋯ = ⋯
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Equations
Equations
- Auto.Embedding.Lam.instToExprLamTerm = { toExpr := Auto.Embedding.Lam.toExprLamTerm✝, toTypeExpr := Lean.Expr.const `Auto.Embedding.Lam.LamTerm [] }
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
- (Auto.Embedding.Lam.LamTerm.app a (Auto.Embedding.Lam.LamTerm.app a_1 (Auto.Embedding.Lam.LamTerm.base (Auto.Embedding.Lam.LamBaseTerm.eq a_2)) a_3) a_4).isMkEq = true
- x✝.isMkEq = false
Instances For
Equations
- (Auto.Embedding.Lam.LamTerm.atom a).size = 1
- (Auto.Embedding.Lam.LamTerm.etom a).size = 1
- (Auto.Embedding.Lam.LamTerm.base a).size = 1
- (Auto.Embedding.Lam.LamTerm.bvar a).size = 1
- (Auto.Embedding.Lam.LamTerm.lam a a_1).size = a_1.size + 1
- (Auto.Embedding.Lam.LamTerm.app a a_1 a_2).size = a_1.size + a_2.size
Instances For
Check whether the term contains loose bound variables idx
levels
above local context root
Equations
- Auto.Embedding.Lam.LamTerm.hasLooseBVarEq idx (Auto.Embedding.Lam.LamTerm.atom a) = false
- Auto.Embedding.Lam.LamTerm.hasLooseBVarEq idx (Auto.Embedding.Lam.LamTerm.etom a) = false
- Auto.Embedding.Lam.LamTerm.hasLooseBVarEq idx (Auto.Embedding.Lam.LamTerm.base a) = false
- Auto.Embedding.Lam.LamTerm.hasLooseBVarEq idx (Auto.Embedding.Lam.LamTerm.bvar a) = idx.beq a
- Auto.Embedding.Lam.LamTerm.hasLooseBVarEq idx (Auto.Embedding.Lam.LamTerm.lam a a_1) = Auto.Embedding.Lam.LamTerm.hasLooseBVarEq idx.succ a_1
- Auto.Embedding.Lam.LamTerm.hasLooseBVarEq idx (Auto.Embedding.Lam.LamTerm.app a a_1 a_2) = (Auto.Embedding.Lam.LamTerm.hasLooseBVarEq idx a_1 || Auto.Embedding.Lam.LamTerm.hasLooseBVarEq idx a_2)
Instances For
Check whether the term contains loose bound variables greater
or equal to idx
levels above local context root
Equations
- Auto.Embedding.Lam.LamTerm.hasLooseBVarGe idx (Auto.Embedding.Lam.LamTerm.atom a) = false
- Auto.Embedding.Lam.LamTerm.hasLooseBVarGe idx (Auto.Embedding.Lam.LamTerm.etom a) = false
- Auto.Embedding.Lam.LamTerm.hasLooseBVarGe idx (Auto.Embedding.Lam.LamTerm.base a) = false
- Auto.Embedding.Lam.LamTerm.hasLooseBVarGe idx (Auto.Embedding.Lam.LamTerm.bvar a) = idx.ble a
- Auto.Embedding.Lam.LamTerm.hasLooseBVarGe idx (Auto.Embedding.Lam.LamTerm.lam a a_1) = Auto.Embedding.Lam.LamTerm.hasLooseBVarGe idx.succ a_1
- Auto.Embedding.Lam.LamTerm.hasLooseBVarGe idx (Auto.Embedding.Lam.LamTerm.app a a_1 a_2) = (Auto.Embedding.Lam.LamTerm.hasLooseBVarGe idx a_1 || Auto.Embedding.Lam.LamTerm.hasLooseBVarGe idx a_2)
Instances For
Instances For
Equations
- (Auto.Embedding.Lam.LamTerm.atom a).maxLooseBVarSucc = 0
- (Auto.Embedding.Lam.LamTerm.etom a).maxLooseBVarSucc = 0
- (Auto.Embedding.Lam.LamTerm.base a).maxLooseBVarSucc = 0
- (Auto.Embedding.Lam.LamTerm.bvar a).maxLooseBVarSucc = a.succ
- (Auto.Embedding.Lam.LamTerm.lam a a_1).maxLooseBVarSucc = a_1.maxLooseBVarSucc.pred
- (Auto.Embedding.Lam.LamTerm.app a a_1 a_2).maxLooseBVarSucc = a_1.maxLooseBVarSucc.max a_2.maxLooseBVarSucc
Instances For
Equations
- (Auto.Embedding.Lam.LamTerm.atom a).maxEVarSucc = 0
- (Auto.Embedding.Lam.LamTerm.etom a).maxEVarSucc = a.succ
- (Auto.Embedding.Lam.LamTerm.base a).maxEVarSucc = 0
- (Auto.Embedding.Lam.LamTerm.bvar a).maxEVarSucc = 0
- (Auto.Embedding.Lam.LamTerm.lam a a_1).maxEVarSucc = a_1.maxEVarSucc
- (Auto.Embedding.Lam.LamTerm.app a a_1 a_2).maxEVarSucc = a_1.maxEVarSucc.max a_2.maxEVarSucc
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- t.flipApp argTy₁ argTy₂ resTy = Auto.Embedding.Lam.LamTerm.app (argTy₁.func (argTy₂.func resTy)) (Auto.Embedding.Lam.LamTerm.flip argTy₁ argTy₂ resTy) t
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Make BitVec.ofNat n i
Equations
- One or more equations did not get rendered due to their size.
Instances For
Make BitVec.ofInt n i
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- t.mkForallEFN [] = t
- t.mkForallEFN (s :: lctx) = Auto.Embedding.Lam.LamTerm.mkForallEF s (t.mkForallEFN lctx)
Instances For
Given λ (_ : ty₀) ⋯ (_ : tyᵢ₋₁), body
, return body
Equations
- (Auto.Embedding.Lam.LamTerm.lam a a_1).getLamBody = a_1.getLamBody
- x✝.getLamBody = x✝
Instances For
Equations
Instances For
Instances For
Instances For
Equations
- Auto.Embedding.Lam.LamTerm.getAppArgsAux args (Auto.Embedding.Lam.LamTerm.app a a_1 a_2) = Auto.Embedding.Lam.LamTerm.getAppArgsAux ((a, a_2) :: args) a_1
- Auto.Embedding.Lam.LamTerm.getAppArgsAux args x✝ = args
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Instances For
Equations
Instances For
Equations
Instances For
Equations
- Auto.Embedding.Lam.LamTerm.getAppArgsNAux Nat.zero args t = some args
- Auto.Embedding.Lam.LamTerm.getAppArgsNAux n_2.succ args (Auto.Embedding.Lam.LamTerm.app a a_1 a_2) = Auto.Embedding.Lam.LamTerm.getAppArgsNAux n_2 ((a, a_2) :: args) a_1
- Auto.Embedding.Lam.LamTerm.getAppArgsNAux n_2.succ args t = none
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Instances For
Equations
Instances For
Equations
- t.bvarAppsRev [] = t
- t.bvarAppsRev (s :: lctx_1) = (Auto.Embedding.Lam.LamTerm.app s t (Auto.Embedding.Lam.LamTerm.bvar lctx_1.length)).bvarAppsRev lctx_1
Instances For
Equations
- One or more equations did not get rendered due to their size.
- t.getForallEFBody = t
Instances For
Equations
- One or more equations did not get rendered due to their size.
- t.getForallEFTys = []
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Auto.Embedding.Lam.instReprLamTerm = { reprPrec := fun (f : Auto.Embedding.Lam.LamTerm) (n : Nat) => f.reprPrec n }
Equations
- (Auto.Embedding.Lam.LamTerm.atom n₁).beq (Auto.Embedding.Lam.LamTerm.atom n₂) = n₁.beq n₂
- (Auto.Embedding.Lam.LamTerm.etom n₁).beq (Auto.Embedding.Lam.LamTerm.etom n₂) = n₁.beq n₂
- (Auto.Embedding.Lam.LamTerm.base b₁).beq (Auto.Embedding.Lam.LamTerm.base b₂) = b₁.beq b₂
- (Auto.Embedding.Lam.LamTerm.bvar n₁).beq (Auto.Embedding.Lam.LamTerm.bvar n₂) = n₁.beq n₂
- (Auto.Embedding.Lam.LamTerm.lam s₁ t₁).beq (Auto.Embedding.Lam.LamTerm.lam s₂ t₂) = (s₁.beq s₂ && t₁.beq t₂)
- (Auto.Embedding.Lam.LamTerm.app s₁ fn₁ arg₁).beq (Auto.Embedding.Lam.LamTerm.app s₂ fn₂ arg₂) = (s₁.beq s₂ && fn₁.beq fn₂ && arg₁.beq arg₂)
- x✝¹.beq x✝ = false
Instances For
Equations
LamTerm.containsSort
has a nice property :
· Let s
be a non-function type. If a term t
satisfies
LamWF ltv ⟨lctx, t, s'⟩
, and s
occurs in neither t
nor s'
, then for all atoms occurring in t
, s
does
not occur in the atom's type.
To see this, notice that the argument type is recorded
in .app
, and the binder type is recorded in .lam
Equations
- (Auto.Embedding.Lam.LamTerm.atom a).containsSort s = false
- (Auto.Embedding.Lam.LamTerm.etom a).containsSort s = false
- (Auto.Embedding.Lam.LamTerm.base a).containsSort s = a.containsSort s
- (Auto.Embedding.Lam.LamTerm.bvar a).containsSort s = false
- (Auto.Embedding.Lam.LamTerm.lam a a_1).containsSort s = (a.contains s || a_1.containsSort s)
- (Auto.Embedding.Lam.LamTerm.app a a_1 a_2).containsSort s = (a.contains s || a_1.containsSort s || a_2.containsSort s)
Instances For
Equations
- One or more equations did not get rendered due to their size.
- Auto.Embedding.Lam.LamTerm.lamCheck? ltv x✝ (Auto.Embedding.Lam.LamTerm.atom n) = some (ltv.lamVarTy n)
- Auto.Embedding.Lam.LamTerm.lamCheck? ltv x✝ (Auto.Embedding.Lam.LamTerm.etom n) = some (ltv.lamEVarTy n)
- Auto.Embedding.Lam.LamTerm.lamCheck? ltv x✝ (Auto.Embedding.Lam.LamTerm.base b) = some (Auto.Embedding.Lam.LamBaseTerm.lamCheck ltv b)
- Auto.Embedding.Lam.LamTerm.lamCheck? ltv x✝ (Auto.Embedding.Lam.LamTerm.bvar n) = some (x✝ n)
Instances For
- ofAtom {ltv : LamTyVal} {lctx : Nat → LamSort} (n : Nat) : LamWF ltv { lctx := lctx, rterm := LamTerm.atom n, rty := ltv.lamVarTy n }
- ofEtom {ltv : LamTyVal} {lctx : Nat → LamSort} (n : Nat) : LamWF ltv { lctx := lctx, rterm := LamTerm.etom n, rty := ltv.lamEVarTy n }
- ofBase {ltv : LamTyVal} {lctx : Nat → LamSort} {b : LamBaseTerm} {s : LamSort} (H : LamBaseTerm.LamWF ltv b s) : LamWF ltv { lctx := lctx, rterm := LamTerm.base b, rty := s }
- ofBVar {ltv : LamTyVal} {lctx : Nat → LamSort} (n : Nat) : LamWF ltv { lctx := lctx, rterm := LamTerm.bvar n, rty := lctx n }
- ofLam {ltv : LamTyVal} {lctx : Nat → LamSort} {argTy : LamSort} (bodyTy : LamSort) {body : LamTerm} (H : LamWF ltv { lctx := pushLCtx argTy lctx, rterm := body, rty := bodyTy }) : LamWF ltv { lctx := lctx, rterm := LamTerm.lam argTy body, rty := argTy.func bodyTy }
- ofApp {ltv : LamTyVal} {lctx : Nat → LamSort} (argTy : LamSort) {resTy : LamSort} {fn arg : LamTerm} (HFn : LamWF ltv { lctx := lctx, rterm := fn, rty := argTy.func resTy }) (HArg : LamWF ltv { lctx := lctx, rterm := arg, rty := argTy }) : LamWF ltv { lctx := lctx, rterm := LamTerm.app argTy fn arg, rty := resTy }
Instances For
Equations
- One or more equations did not get rendered due to their size.
- Auto.Embedding.Lam.LamWF.lctxIrrelevance hirr_2 (Auto.Embedding.Lam.LamWF.ofAtom n) = Auto.Embedding.Lam.LamWF.ofAtom n
- Auto.Embedding.Lam.LamWF.lctxIrrelevance hirr_2 (Auto.Embedding.Lam.LamWF.ofEtom n) = Auto.Embedding.Lam.LamWF.ofEtom n
- Auto.Embedding.Lam.LamWF.lctxIrrelevance hirr_2 (Auto.Embedding.Lam.LamWF.ofBase H) = Auto.Embedding.Lam.LamWF.ofBase H
- Auto.Embedding.Lam.LamWF.lctxIrrelevance hirr_2 (Auto.Embedding.Lam.LamWF.ofBVar n) = ⋯ ▸ Auto.Embedding.Lam.LamWF.ofBVar n
- Auto.Embedding.Lam.LamWF.lctxIrrelevance hirr_2 (Auto.Embedding.Lam.LamWF.ofLam bodyTy H) = Auto.Embedding.Lam.LamWF.ofLam bodyTy (Auto.Embedding.Lam.LamWF.lctxIrrelevance ⋯ H)
Instances For
Equations
- One or more equations did not get rendered due to their size.
- Auto.Embedding.Lam.LamWF.eVarIrrelevance hLamVarTy hLamILTy hirr_2 (Auto.Embedding.Lam.LamWF.ofAtom n) = ⋯ ▸ Auto.Embedding.Lam.LamWF.ofAtom n
- Auto.Embedding.Lam.LamWF.eVarIrrelevance hLamVarTy hLamILTy hirr_2 (Auto.Embedding.Lam.LamWF.ofEtom n) = ⋯ ▸ Auto.Embedding.Lam.LamWF.ofEtom n
- Auto.Embedding.Lam.LamWF.eVarIrrelevance hLamVarTy hLamILTy hirr_2 (Auto.Embedding.Lam.LamWF.ofBVar n) = Auto.Embedding.Lam.LamWF.ofBVar n
Instances For
Equations
Instances For
Equations
- (Auto.Embedding.Lam.LamWF.ofLam argTy HBody).getLam = HBody
Instances For
Equations
- (Auto.Embedding.Lam.LamWF.ofApp argTy HFn HArg).getFn = HFn
Instances For
Equations
- (Auto.Embedding.Lam.LamWF.ofApp argTy HFn HArg).getArg = HArg
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- wft.flipApp = Auto.Embedding.Lam.LamWF.ofApp (argTy₁.func (argTy₂.func resTy)) Auto.Embedding.Lam.LamWF.flip wft
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- wft₁.mkEq wft₂ = Auto.Embedding.Lam.LamWF.ofApp s (Auto.Embedding.Lam.LamWF.ofApp s (Auto.Embedding.Lam.LamWF.ofBase (Auto.Embedding.Lam.LamBaseTerm.LamWF.ofEq s)) wft₁) wft₂
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- wf.fromMkForallEF = wf.getArg.getLam
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- wf.fromMkExistEF = wf.getArg.getLam
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- wfFn_2.mkAppN Auto.HList.nil = wfFn_2
- wfFn_2.mkAppN (Auto.HList.cons HArg HArgs) = (Auto.Embedding.Lam.LamWF.ofApp ty.fst wfFn_2 HArg).mkAppN HArgs
Instances For
Equations
- wfApp_2.fnWFOfMkAppN = wfApp_2
- wfApp_2.fnWFOfMkAppN = wfApp_2.fnWFOfMkAppN.getFn
Instances For
Equations
- wfApp_2.argsWFOfMkAppN = Auto.HList.nil
- wfApp_2.argsWFOfMkAppN = Auto.HList.cons wfApp_2.fnWFOfMkAppN.getArg wfApp_2.argsWFOfMkAppN
Instances For
Equations
- (Auto.Embedding.Lam.LamWF.ofAtom n).getAppFn = ⟨ltv.lamVarTy n, Auto.Embedding.Lam.LamWF.ofAtom n⟩
- (Auto.Embedding.Lam.LamWF.ofEtom n).getAppFn = ⟨ltv.lamEVarTy n, Auto.Embedding.Lam.LamWF.ofEtom n⟩
- (Auto.Embedding.Lam.LamWF.ofBase H).getAppFn = ⟨rty, Auto.Embedding.Lam.LamWF.ofBase H⟩
- (Auto.Embedding.Lam.LamWF.ofBVar n).getAppFn = ⟨lctx n, Auto.Embedding.Lam.LamWF.ofBVar n⟩
- (Auto.Embedding.Lam.LamWF.ofLam s body_1).getAppFn = ⟨argTy.func s, Auto.Embedding.Lam.LamWF.ofLam s body_1⟩
- (Auto.Embedding.Lam.LamWF.ofApp argTy wfFn wfArg).getAppFn = id wfFn.getAppFn
Instances For
Equations
- (Auto.Embedding.Lam.LamWF.ofAtom n).getAppArgs = Auto.HList.nil
- (Auto.Embedding.Lam.LamWF.ofEtom n).getAppArgs = Auto.HList.nil
- (Auto.Embedding.Lam.LamWF.ofBase H).getAppArgs = Auto.HList.nil
- (Auto.Embedding.Lam.LamWF.ofBVar n).getAppArgs = Auto.HList.nil
- (Auto.Embedding.Lam.LamWF.ofLam s_1 body_1).getAppArgs = Auto.HList.nil
- (Auto.Embedding.Lam.LamWF.ofApp argTy wfFn wfArg).getAppArgs = ⋯.mpr (wfFn.getAppArgs.append (Auto.HList.cons wfArg Auto.HList.nil))
Instances For
Equations
- wfp_2.mkLamFN = wfp_2
- wfp_2.mkLamFN = id (Auto.Embedding.Lam.LamWF.ofLam (List.foldr (fun (s cur : Auto.Embedding.Lam.LamSort) => s.func cur) s ls_2) (⋯.mp (⋯.mp wfp_2)).mkLamFN)
Instances For
Equations
- wfLam_2.fromMkLamFN = wfLam_2
- wfLam_2.fromMkLamFN = ⋯.mpr (⋯.mpr wfLam_2.getLam.fromMkLamFN)
Instances For
Equations
- One or more equations did not get rendered due to their size.
- wfLam_2.fromMkLamFN_s_eq_mkFuncs_reverse = ⟨s, ⋯⟩
Instances For
Equations
- wfp_2.mkForallEFN = wfp_2
- wfp_2.mkForallEFN = id (⋯.mp (⋯.mp wfp_2)).mkForallEFN.mkForallEF
Instances For
Equations
- wf_2.fromMkForallEFN = wf_2
- wf_2.fromMkForallEFN = ⋯.mpr (⋯.mpr wf_2.fromMkForallEF.fromMkForallEFN)
Instances For
Equations
- wfp.mkForallEFN' = (⋯.mpr wfp).mkForallEFN
Instances For
Equations
- wf.fromMkForallEFN' = ⋯.mpr wf.fromMkForallEFN
Instances For
Equations
- Auto.Embedding.Lam.LamWF.ofAtom' n s heq = ⋯.mpr (Auto.Embedding.Lam.LamWF.ofAtom n)
Instances For
Equations
- Auto.Embedding.Lam.LamWF.ofEtom' n s heq = ⋯.mpr (Auto.Embedding.Lam.LamWF.ofEtom n)
Instances For
Equations
- Auto.Embedding.Lam.LamWF.ofBVar' n s heq = ⋯.mpr (Auto.Embedding.Lam.LamWF.ofBVar n)
Instances For
Equations
- wft_2.bvarApps = wft_2
- wft_2.bvarApps = Auto.Embedding.Lam.LamWF.ofApp ty wft_2.bvarApps (have tyeq := ⋯; ⋯.mpr (Auto.Embedding.Lam.LamWF.ofBVar ex.length))
Instances For
Equations
- One or more equations did not get rendered due to their size.
- wft_2.bvarAppsRev = wft_2
Instances For
Equations
- One or more equations did not get rendered due to their size.
- wfAp_2.fromBVarAppsRev = wfAp_2
Instances For
Equations
- One or more equations did not get rendered due to their size.
- Auto.Embedding.Lam.LamWF.ofLamTerm (Auto.Embedding.Lam.LamTerm.atom n) = some ⟨ltv.lamVarTy n, Auto.Embedding.Lam.LamWF.ofAtom n⟩
- Auto.Embedding.Lam.LamWF.ofLamTerm (Auto.Embedding.Lam.LamTerm.etom n) = some ⟨ltv.lamEVarTy n, Auto.Embedding.Lam.LamWF.ofEtom n⟩
- Auto.Embedding.Lam.LamWF.ofLamTerm (Auto.Embedding.Lam.LamTerm.bvar n) = some ⟨x✝ n, Auto.Embedding.Lam.LamWF.ofBVar n⟩
Instances For
Equations
- One or more equations did not get rendered due to their size.
- Auto.Embedding.Lam.LamWF.ofLamCheck? x_2 = ⋯.mpr (Auto.Embedding.Lam.LamWF.ofAtom n)
- Auto.Embedding.Lam.LamWF.ofLamCheck? x_2 = ⋯.mpr (Auto.Embedding.Lam.LamWF.ofEtom n)
- Auto.Embedding.Lam.LamWF.ofLamCheck? x_2 = Auto.Embedding.Lam.LamWF.ofBase (Auto.Embedding.Lam.LamBaseTerm.LamWF.ofCheck ⋯)
- Auto.Embedding.Lam.LamWF.ofLamCheck? x_2 = ⋯.mpr (Auto.Embedding.Lam.LamWF.ofBVar n)
Instances For
Equations
- One or more equations did not get rendered due to their size.
- Auto.Embedding.Lam.LamWF.interp lval x✝¹ x✝ (Auto.Embedding.Lam.LamWF.ofAtom n) = lval.varVal n
- Auto.Embedding.Lam.LamWF.interp lval x✝¹ x✝ (Auto.Embedding.Lam.LamWF.ofEtom n) = lval.eVarVal n
- Auto.Embedding.Lam.LamWF.interp lval x✝¹ x✝ (Auto.Embedding.Lam.LamWF.ofBase H) = Auto.Embedding.Lam.LamBaseTerm.LamWF.interp lval H
- Auto.Embedding.Lam.LamWF.interp lval x✝¹ x✝ (Auto.Embedding.Lam.LamWF.ofBVar n) = x✝ n
- Auto.Embedding.Lam.LamWF.interp lval x✝¹ x✝ (Auto.Embedding.Lam.LamWF.ofApp argTy HFn HArg) = Auto.Embedding.Lam.LamWF.interp lval x✝¹ x✝ HFn (Auto.Embedding.Lam.LamWF.interp lval x✝¹ x✝ HArg)