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?
Fixpoint update_value ( n m : nat) (l : list nat): list nat :=
match l with
| nil => 
| h :: t =>
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