Vincent Siles (Apr 01 2021 at 15:29): Vincent Siles (Apr 01 2021 at 15:29):Hi ! I'm testing Equations and have a noob questions:
From Equations Require Import Equations.
From Coq Require Import List.
Import ListNotations.
(* Cannot guess decreasing argument of fix *)
Equations f {A: Type} (a: A) (l:list A) : list A :=
f a [] := [] ;
f a [x] := [x];
f a (hd :: tl) := hd :: a :: f a tl
.
How to specify the decreasing argument ?
Kenji Maillard (Apr 01 2021 at 15:34):You can add an annotation after the type:
Equations f {A: Type} (a: A) (l:list A) : list A by struct l :=
But here equations still complains that the recursion does not happen on the right subterm. You can solve it by making more explicit the structure of pattern-matches:
Equations f {A: Type} (a: A) (l:list A) : list A:=
f a [] := [] ;
f a (hd :: tl) with tl => {
| [] := [hd] ;
| _ := hd :: a :: f a tl
}.
Perfect, thank you @Kenji Maillard
Last updated: Apr 20 2024 at 10:02 UTC