partial def Lean.Syntax.stripPos : Lean.Syntax → Lean.Syntax

structure Qq.Impl.PatVarDecl : Type

• ty : Option Q(Lean.Expr)
• fvarId : Lean.FVarId
• userName : Lean.Name

def Qq.Impl.PatVarDecl.fvarTy : Qq.Impl.PatVarDecl → Q(Type)

Equations

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

def Qq.Impl.mkIsDefEqType : List Qq.Impl.PatVarDecl → Q(Type)

def Qq.Impl.mkLambda' (n : Lean.Name) (fvar : Lean.Expr) (ty : Lean.Expr) (body : Lean.Expr) : Lean.MetaM Lean.Expr

Equations

• Qq.Impl.mkLambda' n fvar ty body = do let __do_lift ← Lean.Expr.abstractM body #[fvar] pure (Lean.mkLambda n Lean.BinderInfo.default ty __do_lift)

def Qq.Impl.mkLet' (n : Lean.Name) (fvar : Lean.Expr) (ty : Lean.Expr) (val : Lean.Expr) (body : Lean.Expr) : Lean.MetaM Lean.Expr

Equations

• Qq.Impl.mkLet' n fvar ty val body = do let __do_lift ← Lean.Expr.abstractM body #[fvar] pure (Lean.mkLet n ty val __do_lift)

def Qq.Impl.replaceTempExprsByQVars : List Qq.Impl.PatVarDecl → Lean.Expr → Lean.Expr

Equations

• One or more equations did not get rendered due to their size.
• Qq.Impl.replaceTempExprsByQVars [] x = x
• Qq.Impl.replaceTempExprsByQVars ({ ty := none, fvarId := fvarId, userName := userName } :: decls) x = Qq.Impl.replaceTempExprsByQVars decls x

def Qq.Impl.unquoteForMatch (et : Lean.Expr) : Qq.Impl.UnquoteM (Lean.LocalContext × Lean.LocalInstances × Lean.Expr)

Equations

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

def Qq.Impl.mkNAryFunctionType : Nat → Lean.MetaM Lean.Expr

Equations

• One or more equations did not get rendered due to their size.
• Qq.Impl.mkNAryFunctionType 0 = Lean.Meta.mkFreshTypeMVar Lean.MetavarKind.natural Lean.Name.anonymous

partial def Qq.Impl.getPatVars (pat : Lean.Term) : StateT (Array (Lean.Name × Nat × Lean.Expr × Lean.Term)) Lean.Elab.TermElabM Lean.Term

def Qq.Impl.getPatVars.isPatVar (fn : Lean.Syntax) : Bool

Equations

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

partial def Qq.Impl.getPatVars.mkMVar (fn : Lean.Syntax) (args : Array Lean.Term) : StateT (Array (Lean.Name × Nat × Lean.Expr × Lean.Term)) Lean.Elab.TermElabM Lean.Term

def Qq.Impl.elabPat (pat : Lean.Term) (lctx : Lean.LocalContext) (localInsts : Lean.LocalInstances) (ty : Lean.Expr) (levelNames : List Lean.Name) : Lean.Elab.TermElabM (Lean.Expr × Array Lean.LocalDecl × Array Lean.Name)

Equations

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

def Qq.Impl.«term_qq_match_←_|_In_» : Lean.ParserDescr

Equations

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

def Qq.Impl.«term_qq_match_←_|_» : Lean.ParserDescr

Equations

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

partial def Qq.Impl.isIrrefutablePattern : Lean.Term → Bool

def Qq.Impl.term_comefrom_Do_In_ : Lean.ParserDescr

Equations

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

def Qq.Impl.term_comefrom_Do_ : Lean.ParserDescr

Equations

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

def Qq.Impl.doElemComefrom_Do_ : Lean.ParserDescr

Equations

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

def Qq.Impl.mkLetDoSeqItem {m : Type → Type} [Monad m] [Lean.MonadQuotation m] (pat : Lean.Term) (rhs : Lean.TSyntax `doElem) (alt : Lean.TSyntax `Lean.Parser.Term.doSeq) : m (List (Lean.TSyntax `Lean.Parser.Term.doSeqItem))

Equations

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

def Qq.«term~q(_)» : Lean.ParserDescr

Equations

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

partial def Qq.Impl.hasQMatch : Lean.Syntax → Bool

partial def Qq.Impl.floatQMatch (alt : Lean.TSyntax `Lean.Parser.Term.doSeq) : Lean.Term → StateT (List (Lean.TSyntax `Lean.Parser.Term.doSeqItem)) Lean.MacroM Lean.Term

partial def Qq.unpackParensIdent : Lean.Syntax → Option Lean.Syntax