inductive DbgResult (α : Type u) : α → Type u

• intro: {α : Type u} → (a b : α) → a = b → DbgResult α a

instance instToStringDbgResult {α : Type u_1} (a : α) : ToString (DbgResult α a)

Equations

• instToStringDbgResult a = { toString := fun (r : DbgResult α a) => match r with | DbgResult.intro a b a => "🎉 Proof Success! 🎉" }

def Qq.rflQ {u : Lean.Level} {α : Q(Sort u)} (a : Q(«$α»)) : Q(«$a» = «$a»)

Equations

• Qq.rflQ a = q(⋯)

def Qq.decideTQ (p : Q(Prop)) : Lean.MetaM Q(«$p»)

Equations

• Qq.decideTQ p = do let dec ← Qq.synthInstanceQ q(Decidable «$p») let h : Q(decide «$p» = true) := Qq.rflQ q(true) pure q(⋯)

def Qq.finQVal {n : Q(ℕ)} (e : Q(Fin «$n»)) : Lean.MetaM (Option ℕ)

Equations

• Qq.finQVal e = do let val ← Lean.Meta.whnf q(↑«$e») let a ← liftM (Lean.Expr.rawNatLit? val) pure (some a)

def Qq.natAppFunQ (f : ℕ → ℕ) (e : Q(ℕ)) : Lean.MetaM Q(ℕ)

Equations

• Qq.natAppFunQ f e = do let e ← Lean.Meta.whnf e match Lean.Expr.rawNatLit? e with | some n => Lean.Expr.ofNat q(ℕ) (f n) | x => Lean.throwError (Lean.toMessageData "not ℕ")

def Qq.inferSortQ' (e : Lean.Expr) : Lean.MetaM ((u : Lean.Level) × (α : let u := u; Q(Sort u)) × Q(«$α»))

Equations

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

def Qq.checkSortQ' (e : Lean.Expr) : Lean.MetaM (Option ((u : Lean.Level) × let u := u; Q(Sort u)))

Equations

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

def Qq.inferPropQ' (e : Lean.Expr) : Lean.MetaM ((p : Q(Prop)) × Q(«$p»))

Equations

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

def Qq.inferPropQ (e : Lean.Expr) : Lean.MetaM Q(Prop)

Equations

• Qq.inferPropQ e = pure e

def Qq.inferSortQOfUniverse' {u : Lean.Level} (e : Lean.Expr) (ty : let u := u; Q(Sort u)) : Lean.MetaM (Option Q(«$ty»))

Equations

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

def Qq.MditeQ {u : Lean.Level} {α : Q(Sort u)} (c : Q(Prop)) (dec : Q(Decidable «$c»)) (t : Lean.MetaM Q(«$c» → «$α»)) (e : Lean.MetaM Q(¬«$c» → «$α»)) : Lean.MetaM Q(«$α»)

Equations

• Qq.MditeQ c dec t e = do let t ← t let e ← e pure q(if h : «$c» then «$t» h else «$e» h)

def Qq.BEqQ {u : Lean.Level} {α : Q(Sort u)} {a : Q(«$α»)} {b : Q(«$α»)} (h : (a == b) = true) : Q(«$a» = «$b»)

Equations

• Qq.BEqQ h = q(⋯)

def Qq.eqQUnsafe {u : Lean.Level} {α : Q(Sort u)} (a : Q(«$α»)) (b : Q(«$α»)) : Q(«$a» = «$b»)

Equations

• Qq.eqQUnsafe a b = q(⋯)

def Qq.toQList {u : Lean.Level} {α : Q(Type u)} : List Q(«$α») → Q(List «$α»)

Equations

• Qq.toQList [] = q([])
• Qq.toQList (a :: v) = let a_1 := Qq.toQList v; let toQList_1 := Qq.toQList v; q(«$a» :: «$toQList_1»)

partial def Qq.ofQList {u : Lean.Level} {α : Q(Type u)} (l : Q(List «$α»)) : Lean.MetaM (List Q(«$α»))

def Qq.isStrongEq (t : Lean.Expr) (s : Lean.Expr) : Lean.MetaM Bool

Equations

• Qq.isStrongEq t s = do let __do_lift ← Lean.Meta.whnf t let __do_lift_1 ← Lean.Meta.whnf s Lean.Meta.isDefEq __do_lift __do_lift_1

def Qq.termEqualTest : Lean.ParserDescr

Equations

• Qq.termEqualTest = Lean.ParserDescr.node `Qq.termEqualTest 1024 (Lean.ParserDescr.symbol "equalTest")

theorem Qq.List.mem_of_eq {α : Type u} {a : α} {b : α} {l : List α} (h : a = b) : a ∈ b :: l

theorem Qq.List.mem_of_mem {α : Type u} {a : α} {b : α} {l : List α} (h : a ∈ l) : a ∈ b :: l

theorem Qq.List.cases_of_mem_cons {α : Type u} {p : α → Prop} {a : α} {a' : α} {l : List α} (h : a' ∈ a :: l) (hl : ∀ a' ∈ l, p a') (ha : p a) : p a'

def Qq.memQList? {u : Lean.Level} {α : Q(Type u)} (a : Q(«$α»)) (l : List Q(«$α»)) : Lean.MetaM (Option (let a_1 := Qq.toQList l; let toQList_1 := Qq.toQList l; Q(«$a» ∈ «$toQList_1»)))

Equations

• One or more equations did not get rendered due to their size.
• Qq.memQList? a [] = pure none

theorem Qq.List.cons_congr {α : Type u} {a : α} {b : α} {l : List α} {k : List α} (ha : a = b) (hl : l = k) : a :: l = b :: k

def Qq.resultList {u : Lean.Level} {α : Q(Type u)} (res : (a : Q(«$α»)) → Lean.MetaM ((res : Q(«$α»)) × Q(«$a» = «$res»))) (l : List Q(«$α»)) : Lean.MetaM ((lres : List Q(«$α»)) × let a := Qq.toQList lres; let a_1 := Qq.toQList l; let toQList_1 := Qq.toQList l; let toQList_2 := Qq.toQList lres; Q(«$toQList_1» = «$toQList_2»))

Equations

• One or more equations did not get rendered due to their size.
• Qq.resultList res [] = pure ⟨[], q(⋯)⟩

def Qq.funResultList {u : Lean.Level} {α : Q(Type u)} {β : Q(Type u)} (f : Q(«$α» → «$β»)) (res : (a : Q(«$α»)) → Lean.MetaM ((res : Q(«$β»)) × Q(«$f» «$a» = «$res»))) (l : List Q(«$α»)) : Lean.MetaM ((lres : List Q(«$β»)) × let a := Qq.toQList lres; let a_1 := Qq.toQList l; let toQList_1 := Qq.toQList l; let toQList_2 := Qq.toQList lres; Q(List.map «$f» «$toQList_1» = «$toQList_2»))

Equations

• One or more equations did not get rendered due to their size.
• Qq.funResultList f res [] = pure ⟨[], q(⋯)⟩

structure Qq.Result {u : Lean.Level} {α : Q(Type u)} (e : Q(«$α»)) : Type

• res : Q(«$α»)
• eq : Q(«$e» = unknown_1)

structure Qq.ResultFun {u : Lean.Level} {v : Lean.Level} {α : Q(Type u)} {β : Q(Type v)} (f : Q(«$α» → «$β»)) (e : Q(«$α»)) : Type

• res : Q(«$β»)
• eq : Q(«$f» «$e» = unknown_1)

def Qq.Result.refl {u : Lean.Level} {α : Q(Type u)} (e : Q(«$α»)) : Qq.Result e

Equations

• Qq.Result.refl e = { res := e, eq := q(⋯) }

def Qq.ResultFun.refl {u : Lean.Level} {v : Lean.Level} {α : Q(Type u)} {β : Q(Type v)} (f : Q(«$α» → «$β»)) (e : Q(«$α»)) : Qq.ResultFun f e

Equations

• Qq.ResultFun.refl f e = { res := q(«$f» «$e»), eq := q(⋯) }

theorem Qq.compVecEmpty {α : Type u} {β : Type v} (f : α → β) : f ∘ ![] = ![]

theorem Qq.compVecCons {α : Type u} {β : Type v} (f : α → β) {n : ℕ} {a : α} {as : Fin n → α} {b : β} {bs : Fin n → β} (hb : f a = b) (hbs : f ∘ as = bs) : f ∘ (a :> as) = b :> bs

theorem Qq.vecConsExt {α : Type u} {n : ℕ} {a : α} {as : Fin n → α} {b : α} {bs : Fin n → α} (hb : a = b) (hbs : as = bs) : a :> as = b :> bs

def Qq.vecFold {u : Lean.Level} (α : Q(Type u)) {n : ℕ} : (Fin n → Q(«$α»)) → Q(Fin «$n» → «$α»)

Equations

• Qq.vecFold α x_2 = q(![])
• Qq.vecFold α v = let ih := Qq.vecFold α fun (x : Fin n) => v x.succ; let a := v 0; let vecFold_1 := Qq.vecFold α fun (x : Fin n) => v x.succ; q(unknown_1 :> «$vecFold_1»)

def Qq.vecFoldDep {u : Lean.Level} {n : ℕ} (α : Q(Fin «$n» → Sort u)) : ((i : Fin n) → Q(«$α» «$i»)) → Q((i : Fin «$n») → «$α» i)

Equations

• One or more equations did not get rendered due to their size.
• Qq.vecFoldDep x_3 x_4 = q(finZeroElim)

def Qq.vecUnfold {u : Lean.Level} (α : Q(Type u)) (n : ℕ) : Q(Fin «$n» → «$α») → Lean.MetaM (Fin n → Q(«$α»))

Equations

• One or more equations did not get rendered due to their size.
• Qq.vecUnfold α 0 x_2 = pure finZeroElim

theorem Qq.eq_cons_app_succ_of_eq {n : ℕ} {α : Type u} {a : α} {b : α} {as : Fin n → α} {i : Fin n} (has : as i = b) : (a :> as) i.succ = b

partial def Qq.vectorGet {u : Lean.Level} {α : Q(Type u)} {n : ℕ} (l : Q(Fin «$n» → «$α»)) (i : Fin n) : Lean.MetaM ((a : Q(«$α»)) × Q(«$l» «$i» = «$a»))

partial def Qq.mapVector {u : Lean.Level} {v : Lean.Level} {α : Q(Type u)} {β : Q(Type v)} (r : Q(«$α») → Lean.MetaM Q(«$β»)) (n : Q(ℕ)) (l : Q(Fin «$n» → «$α»)) : Lean.MetaM Q(Fin «$n» → «$β»)

partial def Qq.resultVectorOfResult {u : Lean.Level} {α : Q(Type u)} (r : (e : Q(«$α»)) → Lean.MetaM ((r : Q(«$α»)) × Q(«$e» = «$r»))) (n : Q(ℕ)) (l : Q(Fin «$n» → «$α»)) : Lean.MetaM ((l' : Q(Fin «$n» → «$α»)) × Q(«$l» = «$l'»))

partial def Qq.resultVectorOfResultFun {u : Lean.Level} {v : Lean.Level} {α : Q(Type u)} {β : Q(Type v)} (f : Q(«$α» → «$β»)) (r : (e : Q(«$α»)) → Lean.MetaM ((r : Q(«$β»)) × Q(«$f» «$e» = «$r»))) (n : Q(ℕ)) (l : Q(Fin «$n» → «$α»)) : Lean.MetaM ((l' : Q(Fin «$n» → «$β»)) × Q(«$f» ∘ «$l» = «$l'»))

partial def Qq.vectorCollection {u : Lean.Level} {v : Lean.Level} {w : Lean.Level} {α : Q(Type u)} {β : Q(Type v)} {H : Q(«$α» → «$β» → Sort w)} (r : (a : Q(«$α»)) → Lean.MetaM ((b : Q(«$β»)) × Q(«$H» «$a» «$b»))) (n : Q(ℕ)) (l : Q(Fin «$n» → «$α»)) : Lean.MetaM ((b : Q(Fin «$n» → «$β»)) × Q((i : Fin «$n») → «$H» («$l» i) («$b» i)))

partial def Qq.mapVectorQ {u : Lean.Level} {v : Lean.Level} {α : Q(Type u)} {β : Q(Type v)} (f : Q(«$α») → Lean.MetaM Q(«$β»)) (n : Q(ℕ)) (l : Q(Fin «$n» → «$α»)) : Lean.MetaM Q(Fin «$n» → «$β»)

def Qq.termDbgmapVectorQ : Lean.ParserDescr

Equations

• Qq.termDbgmapVectorQ = Lean.ParserDescr.node `Qq.termDbgmapVectorQ 1024 (Lean.ParserDescr.symbol "dbgmapVectorQ")

partial def Qq.vectorQNthAux {u : Lean.Level} {α : Q(Type u)} (n : Q(ℕ)) (l : Q(Fin «$n» → «$α»)) (i : ℕ) : Lean.MetaM Q(«$α»)

def Qq.vectorQNth {u : Lean.Level} {α : Q(Type u)} (n : Q(ℕ)) (l : Q(Fin «$n» → «$α»)) (i : Q(Fin «$n»)) : Lean.MetaM ((a : Q(«$α»)) × Q(«$l» «$i» = «$a»))

Equations

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

def Qq.termDbgvectorQNth : Lean.ParserDescr

Equations

• Qq.termDbgvectorQNth = Lean.ParserDescr.node `Qq.termDbgvectorQNth 1024 (Lean.ParserDescr.symbol "dbgvectorQNth")

partial def Qq.vectorAppend {u : Lean.Level} {α : Q(Type u)} (n : Q(ℕ)) (v : Q(Fin «$n» → «$α»)) (a : Q(«$α»)) : Lean.MetaM ((w : Q(Fin («$n» + 1) → «$α»)) × Q(«$v» <: «$a» = «$w»))

def Qq.termDbgVectorAppend : Lean.ParserDescr

Equations

• Qq.termDbgVectorAppend = Lean.ParserDescr.node `Qq.termDbgVectorAppend 1024 (Lean.ParserDescr.symbol "dbgVectorAppend")

def Lean.Expr.stringLit? : Lean.Expr → Option String

Equations

• x.stringLit? = match x with | Lean.Expr.lit (Lean.Literal.strVal s) => some s | x => none

def List.elemM {m : Type → Type v} [inst : Monad m] {α : Type u} (r : α → α → m Bool) (a : α) : List α → m Bool

Equations

• List.elemM r a [] = pure false
• List.elemM r a (b :: bs) = do let __do_lift ← r a b if __do_lift = true then pure true else List.elemM r a bs

class ExprNamed (α : Type) : Type

• name : Q(Type)

instance instExprNamedNat : ExprNamed ℕ

Equations

• instExprNamedNat = { name := q(ℕ) }

instance instExprNamedNat_1 : ExprNamed ℕ

Equations

• instExprNamedNat_1 = { name := q(ℕ) }

class Denotation {u_1 : Lean.Level} (σ : outParam Q(Type u_1)) (α : Type) : Type

• denote' : Q(«$σ») → Lean.MetaM α
• toExpr' : α → Q(«$σ»)

@[reducible, inline]

abbrev Denotation.denote {u_1 : Lean.Level} (σ : Q(Type u_1)) {α : Type} [Denotation σ α] : Q(«$σ») → Lean.MetaM α

Equations

• Denotation.denote σ = Denotation.denote'

@[reducible, inline]

abbrev Denotation.toExpr {u_1 : Lean.Level} (σ : Q(Type u_1)) {α : Type} [Denotation σ α] : α → Q(«$σ»)

Equations

• Denotation.toExpr σ = Denotation.toExpr'

instance Denotation.nat : Denotation q(ℕ) ℕ

Equations

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

instance Denotation.instFin {n : ℕ} : Denotation q(Fin «$n») (Fin n)

Equations

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

instance Denotation.instString : Denotation q(String) String

Equations

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

instance Denotation.list {u_1 : Lean.Level} {σ : Q(Type u_1)} {α : Type} [Denotation σ α] : Denotation q(List «$σ») (List α)

Equations

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

@[reducible, inline]

abbrev Denotation.denoteₗ {u_1 : Lean.Level} {σ : Q(Type u_1)} {α : Type} (d : Denotation σ α) : Q(List «$σ») → Lean.MetaM (List α)

Equations

• d.denoteₗ = Denotation.denote'

@[reducible, inline]

abbrev Denotation.toExprₗ {u_1 : Lean.Level} {σ : Q(Type u_1)} {α : Type} (d : Denotation σ α) : List α → Q(List «$σ»)

Equations

• d.toExprₗ = Denotation.toExpr'

def Denotation.memList? {u_1 : Lean.Level} {α : Type} {σ : Q(Type u_1)} (d : Denotation σ α) (a : α) (l : List α) : Lean.MetaM (Option (let a_1 := d.toExprₗ l; let a := Denotation.toExpr σ a; let toQList_1 := Qq.toQList (List.map Denotation.toExpr' l); Q(unknown_1 ∈ «$toQList_1»)))

Equations

• d.memList? a l = Qq.memQList? (Denotation.toExpr σ a) (List.map Denotation.toExpr' l)

def Denotation.listSigmaImpliment {u_1 : Lean.Level} {α : Type} {σ : Q(Type u_1)} (d : Denotation σ α) {p : Q(«$σ» → Prop)} (l : List ((a : α) × let a := Denotation.toExpr σ a; Q(«$p» unknown_1))) : Lean.MetaM (let a := d.toExprₗ (List.map Sigma.fst l); let toQList_1 := Qq.toQList (List.map Denotation.toExpr' (List.map Sigma.fst l)); Q(∀ a' ∈ «$toQList_1», «$p» a'))

Equations

• d.listSigmaImpliment [] = pure q(⋯)
• d.listSigmaImpliment (⟨a, ha⟩ :: l) = do let ih ← d.listSigmaImpliment l pure (id q(⋯))

def Denotation.isDefEq {u_1 : Lean.Level} {σ : Q(Type u_1)} {α : Type} [Denotation σ α] (a₁ : α) (a₂ : α) : Lean.MetaM Bool

Equations

• Denotation.isDefEq a₁ a₂ = Lean.Meta.isDefEq (Denotation.toExpr σ a₁) (Denotation.toExpr σ a₂)

structure Denotation.DEq {u_1 : Lean.Level} (σ : Q(Type u_1)) {α : Type} [Denotation σ α] (a₁ : α) (a₂ : α) : Type

• expr : let a := Denotation.toExpr σ a₂; let a_1 := Denotation.toExpr σ a₁; Q(unknown_1 = unknown_2)

structure Denotation.DEqFun {u_1 : Lean.Level} {u_2 : Lean.Level} {σ : Q(Type u_1)} {τ : Q(Type u_2)} {α : Type} {β : Type} [Denotation σ α] [Denotation τ β] (f : Q(«$σ» → «$τ»)) (a : α) (b : β) : Type

• expr : let a_1 := Denotation.toExpr τ b; let a := Denotation.toExpr σ a; Q(«$f» unknown_1 = unknown_2)

def Denotation.DEq.refl {u_1 : Lean.Level} {σ : Q(Type u_1)} {α : Type} [Denotation σ α] (a : α) : Denotation.DEq σ a a

Equations

• Denotation.DEq.refl a = { expr := q(⋯) }

def Denotation.DEq.symm {u_1 : Lean.Level} {σ : Q(Type u_1)} {α : Type} [Denotation σ α] {a₁ : α} {a₂ : α} (h : Denotation.DEq σ a₁ a₂) : Denotation.DEq σ a₂ a₁

Equations

• h.symm = { expr := let a := h.expr; q(⋯) }

def Denotation.DEq.trans {u_1 : Lean.Level} {σ : Q(Type u_1)} {α : Type} [Denotation σ α] {a₁ : α} {a₂ : α} {a₃ : α} (h₁ : Denotation.DEq σ a₁ a₂) (h₂ : Denotation.DEq σ a₂ a₃) : Denotation.DEq σ a₁ a₃

Equations

• h₁.trans h₂ = { expr := let a := h₂.expr; let a_1 := h₁.expr; q(⋯) }