I have encountered the following behavior with the Function plugin (FunInd):
Require Import FunInd. Function test0 (n : nat) := (n, n, n). Function test1 (n : nat) := ((n, n), n).
The first definition raises a
funind-cannot-define-graph non-fatal error and does not provide the associated induction lemmas but the second definition works fine.
Is it a known issue with Function or plugins ?
Function has had problems with notations, but I thought it was fixed...
Last updated: Oct 04 2023 at 23:01 UTC