notebook.community

Edit and run 





InΒ [1]:



    


type π“ƒŠ = Bit
type π“‚° = [4]

π“…“π“Šͺ : {𓃀, π“„Ώ} (π“„Ώ -> π“„Ώ) -> [𓃀] π“„Ώ -> [𓃀] π“„Ώ
π“…“π“Šͺ 𓆑 π“‡Œ = [ 𓆑 𓇋 | 𓇋 <- π“‡Œ ]

π“‚€ : {π“„Ώ} π“„Ώ -> π“„Ώ
π“‚€ 𓇋 = 𓇋

π“‚€π“…“π“Šͺ : π“‚° -> π“ƒŠ
property π“‚€π“…“π“Šͺ π“‡Œ = π“‡Œ == π“…“π“Šͺ π“‚€ π“‡Œ



    


















    























InΒ [2]:



    


:prove π“‚€π“…“π“Šͺ



    


















    








Q.E.D.











    























InΒ [Β ]:

Content source: justincampbell/lambdaconf-2015

Similar notebooks:

notebook.community | gallery | about