Stream: Coq users

Topic: Converting list of types to a sum type


view this post on Zulip Julin S (Dec 07 2021 at 04:15):

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].

view this post on Zulip Paolo Giarrusso (Dec 07 2021 at 06:01):

Seems almost a job for fold_right False sum (haven't tried).

view this post on Zulip Paolo Giarrusso (Dec 07 2021 at 06:03):

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: Feb 04 2023 at 22:29 UTC