Stream: Coq users

Topic: Triple in Function

view this post on Zulip Benjamin Bonneau (Dec 16 2022 at 17:07):

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 ?

view this post on Zulip Pierre Courtieu (Dec 16 2022 at 18:48):

Function has had problems with notations, but I thought it was fixed...

Last updated: Oct 13 2024 at 01:02 UTC