inductive Qq.Impl.ExprBackSubstResult : Type

• quoted: Lean.Expr → Qq.Impl.ExprBackSubstResult
• unquoted: Lean.Expr → Qq.Impl.ExprBackSubstResult

inductive Qq.Impl.MVarSynth : Type

• term: Lean.Expr → Lean.MVarId → Qq.Impl.MVarSynth
• type: Lean.MVarId → Qq.Impl.MVarSynth
• level: Lean.LMVarId → Qq.Impl.MVarSynth

structure Qq.Impl.UnquoteState : Type

• mvars : List (Lean.Expr × Qq.Impl.MVarSynth)

  Quoted mvars in the outside lctx (of type Level, Quoted _, or Type). The outside mvars can also be of the form ?m x y z.

• levelSubst : Lean.HashMap Lean.Expr Lean.Level
• exprSubst : Lean.HashMap Lean.Expr Lean.Expr
• unquoted : Lean.LocalContext
• exprBackSubst : Lean.HashMap Lean.Expr Qq.Impl.ExprBackSubstResult
• levelBackSubst : Lean.HashMap Lean.Level Lean.Expr
• abstractedFVars : Array Lean.FVarId

  New free variables in the new context that were newly introduced for irreducible expressions.

• levelNames : List Lean.Name
• mayPostpone : Bool

@[inline, reducible]

abbrev Qq.Impl.UnquoteM (α : Type) : Type

@[inline, reducible]

abbrev Qq.Impl.QuoteM (α : Type) : Type

instance Qq.Impl.instMonadLiftQuoteMUnquoteM : MonadLift Qq.Impl.QuoteM Qq.Impl.UnquoteM

def Qq.Impl.determineLocalInstances (lctx : Lean.LocalContext) : Lean.MetaM Lean.LocalInstances

def Qq.Impl.withUnquotedLCtx {m : Type → Type u_1} {α : Type} [MonadControlT Lean.MetaM m] [Monad m] [MonadLiftT Qq.Impl.QuoteM m] (k : m α) : m α

def Qq.Impl.addDollar : Lean.Name → Lean.Name

Equations

• Qq.Impl.addDollar Lean.Name.anonymous = `«$»
• Qq.Impl.addDollar (Lean.Name.str Lean.Name.anonymous s) = Lean.Name.str Lean.Name.anonymous ("$" ++ s)
• Qq.Impl.addDollar (Lean.Name.str n s) = Lean.Name.str (Qq.Impl.addDollar n) s
• Qq.Impl.addDollar (Lean.Name.num n i) = Lean.Name.num (Qq.Impl.addDollar n) i

def Qq.Impl.removeDollar : Lean.Name → Option Lean.Name

Equations

• Qq.Impl.removeDollar Lean.Name.anonymous = none
• Qq.Impl.removeDollar `«$» = some Lean.Name.anonymous
• Qq.Impl.removeDollar (Lean.Name.str Lean.Name.anonymous s) = if String.startsWith s "$" = true then some (Lean.Name.str Lean.Name.anonymous (String.drop s 1)) else none
• Qq.Impl.removeDollar (Lean.Name.str n s) = Option.map (fun x => Lean.Name.str x s) (Qq.Impl.removeDollar n)
• Qq.Impl.removeDollar (Lean.Name.num n i) = Option.map (fun x => Lean.Name.num x i) (Qq.Impl.removeDollar n)

def Qq.Impl.stripDollars : Lean.Name → Lean.Name

Equations

• One or more equations did not get rendered due to their size.
• Qq.Impl.stripDollars Lean.Name.anonymous = Lean.Name.anonymous
• Qq.Impl.stripDollars (Lean.Name.str n "$") = Qq.Impl.stripDollars n
• Qq.Impl.stripDollars (Lean.Name.str n s) = Lean.Name.str (Qq.Impl.stripDollars n) s
• Qq.Impl.stripDollars (Lean.Name.num n i) = Lean.Name.num (Qq.Impl.stripDollars n) i

def Qq.Impl.addSyntaxDollar : Lean.Syntax → Lean.Syntax

def Qq.Impl.mkAbstractedLevelName (e : Lean.Expr) : Lean.MetaM Lean.Name

def Qq.Impl.isAssignablePattern (e : Lean.Expr) : Lean.MetaM Bool

def Qq.Impl.isBad (e : Lean.Expr) : Bool

partial def Qq.Impl.whnf (e : Lean.Expr) (e0 : optParam Lean.Expr e) : Lean.MetaM Lean.Expr

def Qq.Impl.whnfR (e : Lean.Expr) : Lean.MetaM Lean.Expr

partial def Qq.Impl.unquoteLevel (e : Lean.Expr) : Qq.Impl.UnquoteM Lean.Level

def Qq.Impl.unquoteLevelMVar (mvar : Lean.Expr) : Qq.Impl.UnquoteM Lean.Level

partial def Qq.Impl.unquoteLevelList (e : Lean.Expr) : Qq.Impl.UnquoteM (List Lean.Level)

def Qq.Impl.mkAbstractedName (e : Lean.Expr) : Qq.Impl.UnquoteM Lean.Name

@[inline]

opaque Qq.Impl.betaRev' (e : Lean.Expr) (revArgs : List Lean.Expr) : Lean.Expr

def Qq.Impl.makeZetaReduce (a : Lean.FVarId) (b : Lean.Expr) : Lean.MetaM (Option Lean.LocalContext)

def Qq.Impl.makeDefEq (a : Lean.Expr) (b : Lean.Expr) : Lean.MetaM (Option Lean.LocalContext)

partial def Qq.Impl.unquoteExprList (e : Lean.Expr) : Qq.Impl.UnquoteM (List Lean.Expr)

partial def Qq.Impl.unquoteExprMVar (mvar : Lean.Expr) : Qq.Impl.UnquoteM Lean.Expr

partial def Qq.Impl.unquoteExpr (e : Lean.Expr) : Qq.Impl.UnquoteM Lean.Expr

def Qq.Impl.substLevel (a : Lean.Name) (b : Lean.Level) : Qq.Impl.UnquoteM Unit

def Qq.Impl.unquoteLevelLCtx (addDefEqs : optParam Bool true) : Qq.Impl.UnquoteM Unit

def Qq.Impl.unquoteLCtx : Qq.Impl.UnquoteM Unit

def Qq.Impl.isLevelFVar (n : Lean.Name) : Lean.MetaM (Option Lean.Expr)

def Qq.Impl.quoteLevel : Lean.Level → Qq.Impl.QuoteM Lean.Expr

Equations

• One or more equations did not get rendered due to their size.
• Qq.Impl.quoteLevel Lean.Level.zero = pure (Lean.Expr.const `Lean.Level.zero [])
• Qq.Impl.quoteLevel (Lean.Level.succ u) = do let __do_lift ← Qq.Impl.quoteLevel u pure (Lean.mkApp (Lean.Expr.const `Lean.Level.succ []) __do_lift)

def Qq.Impl.quoteLevelList : List Lean.Level → Qq.Impl.QuoteM Lean.Expr

Equations

• One or more equations did not get rendered due to their size.
• Qq.Impl.quoteLevelList [] = pure (Lean.mkApp (Lean.Expr.const `List.nil [Lean.Level.zero]) (Lean.Expr.const `Lean.Level []))

partial def Qq.Impl.quoteExpr : Lean.Expr → Qq.Impl.QuoteM Lean.Expr

def Qq.Impl.unquoteMVarCore (mvar : Lean.Expr) : Qq.Impl.UnquoteM Unit

def Qq.Impl.unquoteMVar (mvar : Lean.Expr) : Qq.Impl.UnquoteM Unit

def Qq.Impl.MVarSynth.isAssigned : Qq.Impl.MVarSynth → Lean.MetaM Bool

def Qq.Impl.MVarSynth.synth : Qq.Impl.MVarSynth → Qq.Impl.QuoteM Lean.Expr

def Qq.Impl.lctxHasMVar : Lean.MetaM Bool

@[specialize #[]]

def Qq.withProcessPostponed {m : Type → Type u_1} {α : Type} [Monad m] [MonadFinally m] [MonadLiftT Lean.MetaM m] (k : m α) : m α

def Qq.Impl.UnquoteState.withLevelNames {α : Type} (s : Qq.Impl.UnquoteState) (k : Lean.Elab.TermElabM (α × Array Lean.Name)) : Lean.Elab.TermElabM α

def Qq.«termQl(_)» : Lean.ParserDescr

ql(u) quotes the universe level u.

def Qq.«term_=QL_» : Lean.ParserDescr

a =QL b says that the levels a and b are definitionally equal.

def Qq.Impl.macro (t : Lean.Syntax) (expectedType : Lean.Expr) : Lean.Elab.TermElabM Lean.Expr

def Qq.«termQ(__)» : Lean.ParserDescr

q(t) quotes the Lean expression t into a Q(α) (if t : α)

def Qq.«termQ(__)_1» : Lean.ParserDescr

Q(α) is the type of Lean expressions having type α.

def Qq.«term_=Q_» : Lean.TrailingParserDescr

a =Q b says that a and b are definitionally equal.

partial def Qq.Impl.floatLevelAntiquot' {m : Type → Type} [Monad m] [Lean.MonadQuotation m] (stx : Lean.Syntax) : StateT (Array (Lean.Syntax × Lean.Syntax × Lean.Syntax)) m Lean.Syntax

partial def Qq.Impl.floatExprAntiquot' {m : Type → Type} [Monad m] [Lean.MonadQuotation m] (depth : Nat) : Lean.Syntax → StateT (Array (Lean.Syntax × Lean.Syntax × Lean.Syntax)) m Lean.Syntax

def Qq.Impl.floatExprAntiquot {m : Type → Type} [Monad m] [Lean.MonadQuotation m] (depth : Nat) : Lean.Term → StateT (Array (Lean.Ident × Lean.Term × Lean.Term)) m Lean.Term