Stream: Coq users

Topic: replace an element in list


view this post on Zulip Jacob (Mar 31 2021 at 23:46):

How to define an updating function that receives an index, a value and a list of numbers and updates the value of the list at the given index?

view this post on Zulip Jacob (Mar 31 2021 at 23:46):

Fixpoint update_value ( n m : nat) (l : list nat): list nat :=
match l with
| nil => []
| h :: t =>
end.

view this post on Zulip Michael Soegtrop (Apr 01 2021 at 06:48):

You can match on several values at the same time - a convenient short form for a nested match as in

Definition or (a b : bool) :=
match a,b with
| false,false => false
| _,_         => true
end.

You can use this to destruct both the index and the list at the same time. Think of the combined cases the index and the list can have ...


Last updated: Feb 04 2023 at 21:02 UTC