pianke (Feb 18 2023 at 11:35): pianke (Feb 18 2023 at 11:35):Definition l2: =list nat
I have two functions f and f2.
output argument of (f2 a l) & f (f2 a l) is a list nat . Want to write that l2 is equal to the output of f (f2 a l)
Definition f(f2 a l)= l2.
It gives error. Someone plz tell me how to write it?
My main problem is that when define elements in l2 like l2:=[3,4,5,6].
Definition f(f2 a l)= l2, then it works . But don't want to define elements in l2 just call it l2 of type nat.Any nat values may present in it(because values are changing). So that i can write it as Definition f(f2 a l)= l2.
Last updated: Sep 23 2023 at 08:01 UTC