Documentation

Std.Util.TermUnsafe

Defines term syntax to call unsafe functions.

def cool :=
  unsafe (unsafeCast () : Nat)

#eval cool
source
def Std.TermUnsafe.mkAuxName (hint : Lean.Name) :
Lean.Elab.TermElabM Lean.Name

Construct an auxiliary name based on the current declaration name and the given hint base.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Std.TermUnsafe.termUnsafe_ :
    Lean.ParserDescr

    unsafe t : α is an expression constructor which allows using unsafe declarations inside the body of t : α, by creating an auxiliary definition containing t and using implementedBy to wrap it in a safe interface. It is required that α is nonempty for this to be sound, but even beyond that, an unsafe block should be carefully inspected for memory safety because the compiler is unable to guarantee the safety of the operation.

    For example, the evalExpr function is unsafe, because the compiler cannot guarantee that when you call evalExpr Foo ``Foo e that the type Foo corresponds to the name Foo, but in a particular use case, we can ensure this, so unsafe (evalExpr Foo ``Foo e) is a correct usage.

    Equations
    Instances For