In this file, we define the coercion α → Option α.

The use of this coercion is banned in Init and Std (but allowed everwhere else). For this reason, we define it in this file, which must not be imported anywhere in Init or Std (this is enforced by the test importStructure.lean).

instance optionCoe {α : Type u} : Coe α (Option α)

Equations

• optionCoe = { coe := some }