Stream: Coq users

Topic: how to simplify

pianke (Jun 14 2022 at 14:42):

Fixpoint checksum (val: nat) (l: list nat) : nat :=
 match val with
 | O => 0
 | S m' => (f1 val l) + (f2 val l) (checksum m' l)
 end.

I am giving (list_max l +S(a+2)) to above function. I want to ask what will be the value of this function after one iteration. I want to write the output value of this function against given value after one iteration .

Last updated: Feb 06 2023 at 00:03 UTC