The Coq mailing list

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

Two more general questions:

1) Can we build something like this?

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

Here I use f inside the body, but unlikely usual sitations I don't pass it any arguments.

2) In this example I get error about lack of arguments, but in more complex example of my work
I get errors about wrong types like:

term has type Fuel -> ...,
but  expected forall (fuel : Fuel), struct : ?441 -> ...

These errors prompt about this: Is {struct fuel} actually "hardcoded" into termination checking algorithm
or it is just syntactic sugar for some implicit arguments? Can I manually provide such implicit argument?

Sincerely,
Kirill Taran

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

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