Given a list of types, is there a way to convert it to a sum type using sum
?
Like
Require Import List String.
Import ListNotations.
Definition foo := [nat; bool; string]%list.
(*
Compute List.map sum foo.
*)
so that we can apply List.map
or something to get nat + bool + string
out of [nat; bool; string]
.
Seems almost a job for fold_right False sum
(haven't tried).
If you want to avoid the False +
in the result, one could try writing a variant of fold_right, using the the base-case argument just for empty lists...
Last updated: Oct 13 2024 at 01:02 UTC