trees.c.monad.lean

本页保留 Lean 源码及行号。点击行号可定位语句，点击 import 中的模块名可查看依赖。

1import ZlibF.Proof.«deflate.c.engine.loops»
2
3/-! # trees.c: equations for source cut points
4
5These equations only reassociate the existing heap-and-fault monad.
6They do not change its semantics or any translated statement.
7-/
8
9namespace C
10
11/-- Associativity for naming source cut points in the heap-and-fault monad. -/
12theorem M_bind_assoc {α β γ : Type} (m : M α) (f : α → M β) (g : β → M γ) :
13    ((m >>= f) >>= g) = (m >>= fun x => f x >>= g) := by
14  funext h
15  simp only [bind_app]
16  cases m h <;> rfl
17
18/-- A pure source cut point adds no heap effect. -/
19theorem M_pure_bind {α β : Type} (x : α) (f : α → M β) : (pure x >>= f) = f x := by
20  funext h
21  rfl
22
23end C