HepLean Documentation

Init.Data.Option.BasicAux

@[inline]
def Option.get! {α : Type u} [Inhabited α] :
Option αα
Equations
Instances For