Defines term syntax to call unsafe functions.

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

#eval cool

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.

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

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