Stream: Coq users

Topic: how to simplify


view this post on Zulip pianke (Jun 14 2022 at 14:42):

Some time text fix appear before a recursive function ,when it is use by another function. (fix myfunction (a b c : nat) (l : list nat):list nat. It means input parameters are not properly define or pattern matching variable is not clear or output list is not clear. In order to remove it what i should do?


Last updated: Oct 05 2023 at 02:01 UTC