fabian/veribase-idr2 - Change XHAO2M2V7NLRMTG4WWRBOYMD6ACPYALUWGL7ST3PKU5LEH555C2AC

Implement `Data.Optional` `Monad` instance

Created by Fabián Heredia Montiel on May 28, 2021

XHAO2M2V7NLRMTG4WWRBOYMD6ACPYALUWGL7ST3PKU5LEH555C2AC

Dependencies

In channels

main

Change contents

Insertion in src/Data/Optional.idr at line 8 [4.30]
[3.325]
[3.325]
```
import Algebra.Monad
```

Insertion in src/Data/Optional.idr at line 78 [4.30]

[2.591]


public export
Monad Optional where
  bind Nothing  _ = Nothing
  bind (Some x) f = f x
  proofLeftIdentity x f = Refl
  proofRightIdentity Nothing  = Refl
  proofRightIdentity (Some x) = Refl
  proofAssociativity Nothing  f g = Refl
  proofAssociativity (Some x) f g = Refl