|
Last change
on this file since 1784 was
1647,
checked in by tranquil, 9 years ago
|
- corrected some notation problems
- adapted Cligth with slight modifications to new monad framework
|
|
File size:
614 bytes
|
| Line | |
|---|
| 1 | include "utilities/monad.ma". |
|---|
| 2 | include "basics/types.ma". |
|---|
| 3 | |
|---|
| 4 | definition Option ≝ MakeMonadProps |
|---|
| 5 | (* the monad *) |
|---|
| 6 | option |
|---|
| 7 | (* return *) |
|---|
| 8 | (λX.Some X) |
|---|
| 9 | (* bind *) |
|---|
| 10 | (λX,Y,m,f. match m with [ Some x ⇒ f x | None ⇒ None ?]) |
|---|
| 11 | ???. |
|---|
| 12 | // #X[2:#Y#Z]*normalize//qed. |
|---|
| 13 | |
|---|
| 14 | include "hints_declaration.ma". |
|---|
| 15 | unification hint 0 ≔ X; |
|---|
| 16 | N ≟ max_def Option, M ≟ m_def N |
|---|
| 17 | (*---------------*) ⊢ |
|---|
| 18 | option X ≡ monad M X |
|---|
| 19 | . |
|---|
| 20 | |
|---|
| 21 | definition opt_safe : ∀X.∀m : option X. m ≠ None X → X ≝ |
|---|
| 22 | λX,m,prf.match m return λx.m = x → X with |
|---|
| 23 | [ Some t ⇒ λ_.t |
|---|
| 24 | | None ⇒ λeq_m.? |
|---|
| 25 | ] (refl …). elim (absurd … eq_m prf) qed. |
|---|
Note: See
TracBrowser
for help on using the repository browser.
