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

Equations

• Qq.rflQ a = q(⋯)

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

Equations

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

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

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

theorem Qq.List.mem_singleton_of_eq {α : Type u_1} (a b : α) (h : a = b) : a ∈ [b]

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

Equations

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

def Qq.memQList?' (a : Lean.Expr) (l : List Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Equations

• Qq.memQList?' a l = do let __x ← Qq.inferTypeQ' a match __x with | ⟨u, ⟨fst, a⟩⟩ => Qq.memQList? a l

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