I have two different functions whose input argument is natural number list. Before providing the list I want to remove all zeros from it .How I can do it? remove_all function from library may be use for this purpose? Output list of remove_all (lets call it l_f_0) when use by both functions it means it has no zero?
a solution is to use
filterthat keeps elements that verifies some given property.
Require Import List PeanoNat. Compute filter (fun x => negb (x =? 0)) (0 :: 1 :: 0 :: 2 :: nil).
I want to ask if I remove zeros by creating a non-zero list, then use the output list of this function in Coq script. It means list is free of zero? Instead of l I use (remove_zero l) ?
Yes, if you want to call
l without the zeros in
l you can write
(f (remove Nat.eq_dec 0 l)).
Require Import List PeanoNat. Definition l := 0 :: 1 :: 0 :: 2 :: nil. Definition f (l : list nat) := rev l. Check f (remove Nat.eq_dec 0 l). Compute f (remove Nat.eq_dec 0 l).
Last updated: Jan 29 2023 at 06:02 UTC