summary |
shortlog |
log |
commit | commitdiff |
tree
raw |
patch |
inline | side by side (from parent 1:
5e8eadc)
Signed-off-by: Jim Pryor <profjim@jimpryor.net>
Then our unit is naturally:
Then our unit is naturally:
- let s_unit (a : 'a) : ('a state) = fun (s : store) -> (a, s)
+ let s_unit (a : 'a) : 'a state = fun (s : store) -> (a, s)
And we can reason our way to the bind function in a way similar to the reasoning given above. First, we need to apply `f` to the contents of the `u` box:
And we can reason our way to the bind function in a way similar to the reasoning given above. First, we need to apply `f` to the contents of the `u` box: