def tacticUnfold_applicative : Lean.ParserDescr

Equations

• tacticUnfold_applicative = Lean.ParserDescr.node `tacticUnfold_applicative 1024 (Lean.ParserDescr.nonReservedSymbol "unfold_applicative" false)

theorem applicative_none {α β : Type} (f : Option (α → β)) (o : Option α) : f = none → f <*> o = none

theorem applicative_of_none {α β : Type} (f : Option (α → β)) (o : Option α) : o = none → f <*> o = none

theorem applicative_some {α β : Type} (f' : α → β) (v : α) : some f' <*> some v = some (f' v)

theorem applicative_step {α β : Type} (f : α → β) (x : α) : some f <*> some x = some (f x)