Documentation

Init.Control.Basic

def Functor.mapRev {f : Type u → Type v} [inst : Functor f] {α : Type u} {β : Type u} :

f α → (α → β) → f β

Equations

a <&> f = f <$> a

def «term_<&>_» :

Lean.TrailingParserDescr

Equations

«term_<&>_» = Lean.ParserDescr.trailingNode `«term_<&>_» 100 101 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <&> ") (Lean.ParserDescr.cat `term 100))

@[inline]

def Functor.discard {f : Type u → Type v} {α : Type u} [inst : Functor f] (x : f α) :

Equations

discard x = Functor.mapConst PUnit.unit x

class Alternative (f : Type u → Type v) extends Applicative :

Type (max (u + 1) v)

failure : {α : Type u} → f α
orElse : {α : Type u} → f α → (Unit → f α) → f α

Instances

instance instOrElse (f : Type u → Type v) (α : Type u) [inst : Alternative f] :

OrElse (f α)

Equations

instOrElse f α = { orElse := Alternative.orElse }

@[inline]

def guard {f : Type → Type v} [inst : Alternative f] (p : Prop) [inst : Decidable p] :

Equations

guard p = if p then pure () else failure

@[inline]

def optional {f : Type u → Type v} [inst : Alternative f] {α : Type u} (x : f α) :

f (Option α)

Equations

optional x = HOrElse.hOrElse (some <$> x) fun x => pure none

class ToBool (α : Type u) :

Type u

toBool : α → Bool

Instances

instance instToBoolBool :

Equations

instToBoolBool = { toBool := fun b => b }

@[macroInline]

def bool {β : Type u} {α : Type v} [inst : ToBool β] (f : α) (t : α) (b : β) :

α

Equations

bool f t b = match toBool b with | true => t | false => f

@[macroInline]

def orM {m : Type u → Type v} {β : Type u} [inst : Monad m] [inst : ToBool β] (x : m β) (y : m β) :

m β

Equations

(x <||> y) = do let b ← x match toBool b with | true => pure b | false => y

def «term_<||>_» :

Lean.TrailingParserDescr

Equations

«term_<||>_» = Lean.ParserDescr.trailingNode `«term_<||>_» 30 31 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <||> ") (Lean.ParserDescr.cat `term 30))

@[macroInline]

def andM {m : Type u → Type v} {β : Type u} [inst : Monad m] [inst : ToBool β] (x : m β) (y : m β) :

m β

Equations

(x <&&> y) = do let b ← x match toBool b with | true => y | false => pure b

def «term_<&&>_» :

Lean.TrailingParserDescr

Equations

«term_<&&>_» = Lean.ParserDescr.trailingNode `«term_<&&>_» 35 36 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <&&> ") (Lean.ParserDescr.cat `term 35))

@[macroInline]

def notM {m : Type → Type v} [inst : Applicative m] (x : m Bool) :

Equations

notM x = not <$> x

class MonadControl (m : Type u → Type v) (n : Type u → Type w) :

Type (max (max (u + 1) v) w)

stM : Type u → Type u
liftWith : {α : Type u} → (({β : Type u} → n β → m (stM β)) → m α) → n α
restoreM : {α : Type u} → m (stM α) → n α

Instances

class MonadControlT (m : Type u → Type v) (n : Type u → Type w) :

Type (max (max (u + 1) v) w)

stM : Type u → Type u
liftWith : {α : Type u} → (({β : Type u} → n β → m (stM β)) → m α) → n α
restoreM : {α : Type u} → stM α → n α

Instances

instance instMonadControlT (m : Type u_1 → Type u_2) (n : Type u_1 → Type u_3) (o : Type u_1 → Type u_4) [inst : MonadControl n o] [inst : MonadControlT m n] :

MonadControlT m o

Equations

instMonadControlT m n o = { stM := fun α => stM m n (MonadControl.stM n o α), liftWith := fun {α} f => MonadControl.liftWith fun x₂ => liftWith fun x₁ => f fun {β} => x₁ (MonadControl.stM n o β) ∘ x₂ β, restoreM := fun {α} => MonadControl.restoreM ∘ restoreM }

instance instMonadControlT_1 (m : Type u → Type v) [inst : Pure m] :

MonadControlT m m

Equations

instMonadControlT_1 m = { stM := fun α => α, liftWith := fun {α} f => f fun {β} x => x, restoreM := fun {α} x => pure x }

@[inline]

def controlAt (m : Type u → Type v) {n : Type u → Type w} [s1 : MonadControlT m n] [s2 : Bind n] {α : Type u} (f : ({β : Type u} → n β → m (stM m n β)) → m (stM m n α)) :

n α

Equations

controlAt m f = liftWith f >>= restoreM

@[inline]

def control {m : Type u → Type v} {n : Type u → Type w} [inst : MonadControlT m n] [inst : Bind n] {α : Type u} (f : ({β : Type u} → n β → m (stM m n β)) → m (stM m n α)) :

n α

Equations

control f = controlAt m f

class ForM (m : Type u → Type v) (γ : Type w₁) (α : outParam (Type w₂)) :

Type (max (max (max (u + 1) v) w₁) w₂)

forM : [inst : Monad m] → γ → (α → m PUnit) → m PUnit

Instances