The Coq mailing list

[Kirill Taran <kirill.t256 AT gmail.com>]

Well, when I tried to reduce example I succeeded with very small function:

(*  OK  *) Fixpoint f (f : Fuel) {struct f} : Either Error nat :=
  let g := (pure 1) >>= (fun x => pure (S x)) in g fuel.

(* FAIL *) Fixpoint f : forall (f : Fuel) {struct f}, Either Error nat :=
  (pure 1) >>= (fun x => pure (S x)).

(* FAIL *) Fixpoint f : Dirty nat := (pure 1) >>= (fun x => pure (S x)).

But I still can't succed with complex example.

P.S. Here Dirty T = Fuel -> Either Error T.

Sincerely,
Kirill Taran

On Wed, Mar 19, 2014 at 4:50 PM, Kirill Taran <kirill.t256 AT gmail.com> wrote:

Hello.

Can I make Coq to unify forall (x : X) {struct x}, A with T A, where T a := X -> A?
I need this type synonym for usage of some of my type classes, so I can't unwrap T A;
but I need to specify decreasing argument for my fixpoint definition.

Can I resolve that?

Sincerely,
Kirill Taran