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 : Qq.Quoted α) => e }
      Equations
      Equations
      @[reducible, inline]
      abbrev Qq.Quoted.ty {α : Lean.Expr} (t : Qq.Quoted α) :

      Gets the type of a quoted expression.

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

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

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

        • unsafeIntro :: (
          • )
          Instances For

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

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

            • unsafeIntro :: (
              • )
              Instances For

                Check that a term e : Q(α) really has type α.

                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) :

                  Check that the claim $lhs =Q $rhs is actually true; that the two terms are defeq.

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

                    Check that the claim $u =QL $v is actually true; that the two levels are defeq.

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