Closed alexkeizer closed 1 year ago
If a variable α : Type u implements ToExpr, then add it to the context available inside q(...) and Q(...), with the quoted value of ToExpr.toTypeExpr.
α : Type u
ToExpr
q(...)
Q(...)
ToExpr.toTypeExpr
This resolves #9, enabling us to write, e.g.,
import Qq open Qq Lean def listToExpr {α : Type} [ToExpr α] : List α → Q(List $α) | [] => q([]) | a :: as => q($a :: $(listToExpr as))
If a variable
α : Type uimplementsToExpr, then add it to the context available insideq(...)andQ(...), with the quoted value ofToExpr.toTypeExpr.This resolves #9, enabling us to write, e.g.,