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 ls => SOME(x::ls) | NONE => NONE)`; Cheers, Ramana ------------------------------------------------------------------------------ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
