Stream: Coq users

Topic: execute example

view this post on Zulip pianke (Feb 02 2023 at 16:24):

I have plus function from standard library. I am computing below one
Compute (map (fun x => plus 3 x) [2;0;2]). error " The type of this term is a product
while it is expected to be (list nat)." How i should write it?

view this post on Zulip Olivier Laurent (Feb 03 2023 at 11:13):

You do not provide enough context information since basically this works:

Require Import List.
Import ListNotations.

Compute (map (fun x => plus 3 x) [2;0;2]).
(*
     = [5; 3; 5]
     : list nat
*)

Last updated: Oct 04 2023 at 23:01 UTC