Documentation

Qq.Typ

Quoted α is the type of Lean expressions having type α.

You should usually write this using the notation Q($α).

Equations
Instances For

    Creates a quoted expression. Requires that e has type α.

    You should usually write this using the notation q($e).

    Equations
    Instances For
      instance Qq.instBEqQuoted {α : Lean.Expr} :
      Equations
      Equations
      Equations
      Equations
      Equations
      Equations
      • Qq.instCoeOutQuotedExpr = { coe := fun e => e }
      Equations
      Equations
      @[inline, reducible]
      abbrev Qq.Quoted.ty {α : Lean.Expr} (t : Qq.Quoted α) :

      Gets the type of a quoted expression.

      Equations
      Instances For
        structure Qq.QuotedDefEq {u : Lean.Level} {α : Qq.Quoted (Lean.Expr.sort u)} (lhs : Qq.Quoted α) (rhs : Qq.Quoted α) :
        • unsafeIntro :: (
          • )

          QuotedDefEq lhs rhs says that the expressions lhs and rhs are definitionally equal.

          You should usually write this using the notation $lhs =Q $rhs.

          Instances For
            • unsafeIntro :: (
              • )

              QuotedLevelDefEq u v says that the levels u and v are definitionally equal.

              You should usually write this using the notation $u =QL $v.

              Instances For
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  def Qq.QuotedDefEq.check {u : Lean.Level} {α : Qq.Quoted (Lean.Expr.sort u)} {lhs : Qq.Quoted α} {rhs : Qq.Quoted α} (e : Qq.QuotedDefEq lhs rhs) :
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For