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
.
- quoted (e : Lean.Expr) : ExprBackSubstResult
- unquoted (e : Lean.Expr) : ExprBackSubstResult
Instances For
- term (quotedType : Lean.Expr) (unquotedMVar : Lean.MVarId) : MVarSynth
- type (unquotedMVar : Lean.MVarId) : MVarSynth
- level (unquotedMVar : Lean.LMVarId) : MVarSynth
Instances For
Quoted mvars in the outside lctx (of type
Level
,Quoted _
, orType
). 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.
- mayPostpone : Bool
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
a =QL b
says that the levels a
and b
are definitionally equal.
Equations
Instances For
Equations
Instances For
q(t)
quotes the Lean expression t
into a Q(α)
(if t : α
)
Equations
Instances For
Q(α)
is the type of Lean expressions having type α
.
Equations
Instances For
a =Q b
says that a
and b
are definitionally equal.