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

• x.fvarTy = match x with | { ty := none, fvarId := fvarId, userName := userName } => q(Lean.Level) | { ty := some val, fvarId := fvarId, userName := userName } => q(Lean.Expr)

def Qq.Impl.PatVarDecl.fvar (decl : Qq.Impl.PatVarDecl) : let a := decl.fvarTy; let match_1_1 := match decl with | { ty := none, fvarId := fvarId, userName := userName } => q(Lean.Level) | { ty := some val, fvarId := fvarId, userName := userName } => q(Lean.Expr); Q(«$match_1_1»)

Equations

• decl.fvar = Lean.Expr.fvar decl.fvarId

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

Equations

• One or more equations did not get rendered due to their size.
• Qq.Impl.mkIsDefEqType [] = q(Bool)

def Qq.Impl.mkIsDefEqResult (val : Bool) (decls : List Qq.Impl.PatVarDecl) : let a := Qq.Impl.mkIsDefEqType decls; let mkIsDefEqType_1 := Qq.Impl.mkIsDefEqType decls; Q(«$mkIsDefEqType_1»)

def Qq.Impl.mkIsDefEqResultVal (decls : List Qq.Impl.PatVarDecl) : (let a := Qq.Impl.mkIsDefEqType decls; let mkIsDefEqType_1 := Qq.Impl.mkIsDefEqType decls; Q(«$mkIsDefEqType_1»)) → Q(Bool)

Equations

• Qq.Impl.mkIsDefEqResultVal [] val = q(«$val»)
• Qq.Impl.mkIsDefEqResultVal (head :: decls) val = Qq.Impl.mkIsDefEqResultVal decls q(«$val».snd)

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 ← body.abstractM #[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 ← body.abstractM #[fvar] pure (Lean.mkLet n ty val __do_lift)

def Qq.Impl.mkInstantiateMVars (decls : List Qq.Impl.PatVarDecl) : List Qq.Impl.PatVarDecl → Lean.MetaM (let a := Qq.Impl.mkIsDefEqType decls; let mkIsDefEqType_1 := Qq.Impl.mkIsDefEqType decls; Q(Lean.MetaM «$mkIsDefEqType_1»))

def Qq.Impl.mkIsDefEqCore (decls : List Qq.Impl.PatVarDecl) (pat : Q(Lean.Expr)) (discr : Q(Lean.Expr)) : List Qq.Impl.PatVarDecl → Lean.MetaM (let a := Qq.Impl.mkIsDefEqType decls; let mkIsDefEqType_1 := Qq.Impl.mkIsDefEqType decls; Q(Lean.MetaM «$mkIsDefEqType_1»))

Equations

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

def Qq.Impl.mkIsDefEq (decls : List Qq.Impl.PatVarDecl) (pat : Q(Lean.Expr)) (discr : Q(Lean.Expr)) : Lean.MetaM (let a := Qq.Impl.mkIsDefEqType decls; let mkIsDefEqType_1 := Qq.Impl.mkIsDefEqType decls; Q(Lean.MetaM «$mkIsDefEqType_1»))

Equations

• Qq.Impl.mkIsDefEq decls pat discr = do let __do_lift ← Qq.Impl.mkIsDefEqCore decls pat discr decls pure (let a := __do_lift; q(Lean.Meta.withNewMCtxDepth «$__do_lift»))

def Qq.Impl.mkQqLets {γ : Q(Type)} (decls : List Qq.Impl.PatVarDecl) : (let a := Qq.Impl.mkIsDefEqType decls; let mkIsDefEqType_1 := Qq.Impl.mkIsDefEqType decls; Q(«$mkIsDefEqType_1»)) → Lean.Elab.TermElabM Q(«$γ») → Lean.Elab.TermElabM Q(«$γ»)

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.makeMatchCode {v : Lean.Level} {γ : Q(Type)} {m : Q(Type → Type v)} (_instLift : Q(MonadLiftT Lean.MetaM «$m»)) (_instBind : Q(Bind «$m»)) (decls : List Qq.Impl.PatVarDecl) (uTy : Q(Lean.Level)) (ty : Q(Q(Sort «$uTy»))) (pat : Q(Q(«$$ty»))) (discr : Q(Q(«$$ty»))) (alt : Q(«$m» «$γ»)) (expectedType : Lean.Expr) (k : Lean.Expr → Lean.Elab.TermElabM Q(«$m» «$γ»)) : Lean.Elab.TermElabM Q(«$m» «$γ»)

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

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

• Qq.Impl.getPatVars.isPatVar fn = (fn.isAntiquot && !fn.isEscapedAntiquot && fn.getAntiquotTerm.isIdent && fn.getAntiquotTerm.getId.isAtomic)

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 `term) (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