Supporting results for pointwise provable equality.

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

The rfl Q construction in Qq.

Equations

• PointwiseComposition.Qq.rflQ a = q(⋯)

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

The to QList construction in Qq.

Equations

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

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

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

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

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

The mem QList? construction in Qq.

Equations

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

def PointwiseComposition.Qq.memQListOptional' (a : Lean.Expr) (l : List Lean.Expr) : Lean.MetaM (Option Lean.Expr)

The mem QList?' construction in Qq.

Equations

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

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

The of QList construction in Qq.

Equations

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