Defines term syntax to call unsafe functions.
def cool := unsafe (unsafeCast () : Nat) #eval cool
unsafe t : α is an expression constructor which allows using unsafe declarations inside the
t : α, by creating an auxiliary definition containing
t and using
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
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.
- One or more equations did not get rendered due to their size.