Re: [Hol-info] map_option

Hi Ramana, It's rather a similar situation to what I wrote about in http://users.cecs.anu.edu.au/~jeremy/pubs/fgc/fgs/fgs.pdf and also http://users.cecs.anu.edu.au/~jeremy/pubs/fgc/cats/fgc.ps except that I seem to have used sets instead of lists (which I don't think should make a

Re: [Hol-info] map_option

Hi Jeremy, Thanks for the links and information. It's rather more than I was expecting. Do you (or anyone on list) think that function deserves a place (perhaps under a different name) in optionTheory? Cheers, Ramana On 25 September 2015 at 21:21, Jeremy Dawson wrote:

[Hol-info] map_option

Hi all, I think this must be some neat combination of category theory things. Does anyone know which? Or if it's already defined somewhere? val map_option_def = Define` (map_option [] = SOME []) ∧ (map_option (NONE::_) = NONE) ∧ (map_option (SOME x::ls) = case map_option ls of | SOME