LawfulMonadLift

📁 Source: Batteries/Lean/LawfulMonadLift.lean

Statistics

Metric	Count
Definitions	0
Theorems adapt_bind, adapt_pure, lift_bind, lift_pure, instLawfulMonadLiftBaseIOEIO_batteries, instLawfulMonadLiftIOCoreM_batteries, instLawfulMonadLiftSTEST_batteries, instLawfulMonadLiftTCoreMMetaM_batteries, instLawfulMonadLiftTEIOExceptionCommandElabM_batteries, instLawfulMonadLiftTEIOExceptionCoreM_batteries, instLawfulMonadLiftTMetaMTermElabM_batteries, instLawfulMonadLiftTTermElabMTacticM_batteries	12
Total	12

EIO

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adapt_bind 📖	—	—	—	—	—
adapt_pure 📖	—	—	—	—	—

StateRefT'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lift_bind 📖	—	—	—	—	—
lift_pure 📖	—	—	—	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instLawfulMonadLiftBaseIOEIO_batteries 📖	—	—	—	—	—
instLawfulMonadLiftIOCoreM_batteries 📖	—	—	—	—	EIO.adapt_pure StateRefT'.lift_pure EIO.adapt_bind StateRefT'.lift_bind
instLawfulMonadLiftSTEST_batteries 📖	—	—	—	—	—
instLawfulMonadLiftTCoreMMetaM_batteries 📖	—	—	—	—	—
instLawfulMonadLiftTEIOExceptionCommandElabM_batteries 📖	—	—	—	—	—
instLawfulMonadLiftTEIOExceptionCoreM_batteries 📖	—	—	—	—	—
instLawfulMonadLiftTMetaMTermElabM_batteries 📖	—	—	—	—	—
instLawfulMonadLiftTTermElabMTacticM_batteries 📖	—	—	—	—	—

---

← Back to Index