Stream: Coq users

Topic: repeat function


view this post on Zulip zohaze (Mar 14 2022 at 17:56):

I am splitting a natural number list at particular position then pass first five numbers to Coq code to perform different function on it. Result is fine. Now want to repeat same function on next five elements of the list and so on. What command I should use and how I should apply it?

view this post on Zulip Pierre Castéran (Mar 14 2022 at 20:31):

The following code is written under two assumptions (which can be changed)

Require Import List.

Fixpoint take_five {A B} (f : A -> A -> A -> A -> A -> B)
         (l: list A) : list B :=
  match  l with
    (a:: b :: c:: d :: e:: rest) =>  f a b c d e :: take_five f rest
  | _ => nil
  end.

Fixpoint iota n :=
  match n with
    0 => nil
  | S p => n:: iota p
  end.

Compute take_five  (fun a b c d e =>  (a , e)) (List.rev (iota 17)).

view this post on Zulip zohaze (Mar 15 2022 at 18:04):

Thank you. There are multiple functions in the code . It might be difficult to do above for each and every function.
Is there any command which I can apply on whole block of code(which i want to repeat) ? Simply command repeat all functions on specific input and when input change then do the same as multiple time as user define it. Secondly, instead of pair ,may I get list of five elements.


Last updated: Feb 04 2023 at 23:02 UTC