AlternativeMonad

📁 Source: Batteries/Control/AlternativeMonad.lean

Statistics

Metric	Count
Definitions AlternativeMonad, toAlternative, toBind, toMonad, LawfulAlternative, LawfulAlternativeLift, instAlternativeMonad, instAlternativeMonadOfMonad, instAlternativeMonad, instAlternativeMonad, instAlternativeMonad	11
Theorems failure_orElse, failure_seq, map_failure, map_orElse, orElse_assoc, orElse_failure, toLawfulApplicative, monadLift_failure, monadLift_orElse, instLawfulAlternative, instLawfulAlternativeOfLawfulMonad, instLawfulAlternative, instLawfulAlternativeLift, instLawfulAlternative, instLawfulAlternativeLift, instLawfulAlternativeLiftOfLawfulAlternativeOfLawfulMonad, instLawfulAlternativeOfLawfulMonad, failure_bind, failure_seqLeft, failure_seqRight, mapConst_failure, mapConst_orElse, seq_failure	23
Total	34

AlternativeMonad

Definitions

Name	Category	Theorems
toAlternative 📖	CompOp	8 math math: StateRefT'.instLawfulAlternative, failure_bind, ReaderT.instLawfulAlternativeLift, ReaderT.instLawfulAlternative, StateT.instLawfulAlternativeLiftOfLawfulAlternativeOfLawfulMonad, seq_failure, StateT.instLawfulAlternativeOfLawfulMonad, StateRefT'.instLawfulAlternativeLift
toBind 📖	CompOp	—
toMonad 📖	CompOp	7 math math: StateRefT'.instLawfulAlternative, failure_bind, ReaderT.instLawfulAlternativeLift, ReaderT.instLawfulAlternative, StateT.instLawfulAlternativeLiftOfLawfulAlternativeOfLawfulMonad, StateT.instLawfulAlternativeOfLawfulMonad, StateRefT'.instLawfulAlternativeLift

LawfulAlternative

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
failure_orElse 📖	—	—	—	—	—
failure_seq 📖	—	—	—	—	—
map_failure 📖	—	—	—	—	—
map_orElse 📖	—	—	—	—	—
orElse_assoc 📖	—	—	—	—	—
orElse_failure 📖	—	—	—	—	—
toLawfulApplicative 📖	—	—	—	—	—

LawfulAlternativeLift

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
monadLift_failure 📖	—	—	—	—	—
monadLift_orElse 📖	—	—	—	—	—

Option

Definitions

Name	Category	Theorems
instAlternativeMonad 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instLawfulAlternative 📖	mathematical	—	LawfulAlternative	—	—

OptionT

Definitions

Name	Category	Theorems
instAlternativeMonadOfMonad 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instLawfulAlternativeOfLawfulMonad 📖	mathematical	—	LawfulAlternative	—	—

ReaderT

Definitions

Name	Category	Theorems
instAlternativeMonad 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instLawfulAlternative 📖	mathematical	—	LawfulAlternative AlternativeMonad.toAlternative AlternativeMonad.toMonad	—	LawfulAlternative.toLawfulApplicative LawfulAlternative.map_failure LawfulAlternative.failure_seq LawfulAlternative.orElse_failure LawfulAlternative.failure_orElse LawfulAlternative.orElse_assoc run_orElse LawfulAlternative.map_orElse
instLawfulAlternativeLift 📖	mathematical	—	LawfulAlternativeLift AlternativeMonad.toAlternative AlternativeMonad.toMonad	—	run_failure run_orElse

StateRefT'

Definitions

Name	Category	Theorems
instAlternativeMonad 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instLawfulAlternative 📖	mathematical	—	LawfulAlternative AlternativeMonad.toAlternative AlternativeMonad.toMonad	—	ReaderT.instLawfulAlternative
instLawfulAlternativeLift 📖	mathematical	—	LawfulAlternativeLift AlternativeMonad.toAlternative AlternativeMonad.toMonad	—	ReaderT.instLawfulAlternativeLift

StateT

Definitions

Name	Category	Theorems
instAlternativeMonad 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instLawfulAlternativeLiftOfLawfulAlternativeOfLawfulMonad 📖	mathematical	—	LawfulAlternativeLift AlternativeMonad.toAlternative AlternativeMonad.toMonad	—	LawfulAlternative.map_failure run_failure LawfulAlternative.map_orElse run_orElse
instLawfulAlternativeOfLawfulMonad 📖	mathematical	—	LawfulAlternative AlternativeMonad.toMonad AlternativeMonad.toAlternative	—	run_failure LawfulAlternative.map_failure failure_bind LawfulAlternative.orElse_failure LawfulAlternative.failure_orElse LawfulAlternative.orElse_assoc run_orElse LawfulAlternative.map_orElse

(root)

Definitions

Name	Category	Theorems
AlternativeMonad 📖	CompData	—
LawfulAlternative 📖	CompData	5 math math: StateRefT'.instLawfulAlternative, Option.instLawfulAlternative, ReaderT.instLawfulAlternative, OptionT.instLawfulAlternativeOfLawfulMonad, StateT.instLawfulAlternativeOfLawfulMonad
LawfulAlternativeLift 📖	CompData	3 math math: ReaderT.instLawfulAlternativeLift, StateT.instLawfulAlternativeLiftOfLawfulAlternativeOfLawfulMonad, StateRefT'.instLawfulAlternativeLift

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
failure_bind 📖	mathematical	—	AlternativeMonad.toMonad AlternativeMonad.toAlternative	—	LawfulAlternative.map_failure
failure_seqLeft 📖	—	—	—	—	LawfulAlternative.toLawfulApplicative LawfulAlternative.map_failure LawfulAlternative.failure_seq
failure_seqRight 📖	—	—	—	—	LawfulAlternative.toLawfulApplicative LawfulAlternative.map_failure LawfulAlternative.failure_seq
mapConst_failure 📖	—	—	—	—	LawfulAlternative.toLawfulApplicative LawfulAlternative.map_failure
mapConst_orElse 📖	—	—	—	—	LawfulAlternative.toLawfulApplicative LawfulAlternative.map_orElse
seq_failure 📖	mathematical	—	AlternativeMonad.toAlternative	—	LawfulAlternative.map_failure LawfulAlternative.toLawfulApplicative

---

← Back to Index