The q( ) and Q( ) macros

This file provides the main feature of Qq; the q( ) and Q( ) macros, which are available with open scoped Qq.

inductive Qq.Impl.ExprBackSubstResult : Type

• quoted (e : Lean.Expr) : ExprBackSubstResult
• unquoted (e : Lean.Expr) : ExprBackSubstResult

inductive Qq.Impl.MVarSynth : Type

• term (quotedType : Lean.Expr) (unquotedMVar : Lean.MVarId) : MVarSynth
• type (unquotedMVar : Lean.MVarId) : MVarSynth
• level (unquotedMVar : Lean.LMVarId) : MVarSynth

structure Qq.Impl.UnquoteState : Type

• mvars : List (Lean.Expr × 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 : Std.HashMap Lean.Expr Lean.Level

  Maps quoted expressions (of type Level) in the old context to level parameter names in the new context

• exprSubst : Std.HashMap Lean.Expr Lean.Expr

  Maps quoted expressions (of type Expr) in the old context to expressions in the new context

• unquoted : Lean.LocalContext

  New unquoted local context

• exprBackSubst : Std.HashMap Lean.Expr ExprBackSubstResult

  Maps free variables in the new context to expressions in the old context (of type Expr)

• levelBackSubst : Std.HashMap Lean.Level Lean.Expr

  Maps free variables in the new context to levels in the old context (of type Level)

• abstractedFVars : Array Lean.FVarId

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

• levelNames : List Lean.Name
• mayPostpone : Bool

@[reducible, inline]

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

@[reducible, inline]

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

@[implicit_reducible]

instance Qq.Impl.instMonadLiftQuoteMUnquoteM : MonadLift QuoteM 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 QuoteM m] (k : m α) : m α

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

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

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

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 : 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) : UnquoteM Lean.Level

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

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

def Qq.Impl.mkAbstractedName (e : Lean.Expr) : 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 b : Lean.Expr) : Lean.MetaM (Option Lean.LocalContext)

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

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

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

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

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

def Qq.Impl.unquoteLCtx : UnquoteM Unit

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

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

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

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

def Qq.Impl.quoteLCtx (ctx : Lean.LocalContext) (levelNames : List Lean.Name) : UnquoteM (Lean.LocalContext × Array Lean.Expr)

Translates an arbitrary local context to a context of Q-annotated expressions. Used by by_elabq and run_tacq.

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

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

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

def Qq.Impl.MVarSynth.synth : MVarSynth → 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 : 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