Jacob (Mar 31 2021 at 23:46): 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?
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.
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: Apr 18 2024 at 02:01 UTC