Defining recursive Monadic functions

[acjf3]

The following fails:

Define run n = \s. if 0 < n then run (n - 1n) s else ()

giving the error

Defn.prim_mk_defn:
at Defn.prim_mk_defn:
failure in internal translation to tupled format

Clearly the equivalent definition:

Define run n s = if 0 < n then run (n - 1n) s else ()

is fine.

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.

[mn200]

I agree it's a bug, and it's clear why it happens: TFL thinks the function has arity 1 on the left, and then sees it with arity 2 on the right. I guess a fix might be to automatically convert definitions with abstractions on the right into ones where the bound variable moves from the abstraction to the LHS. Someone with copious amounts of spare time might be able to fix this relatively straightforwardly.

[mn200]

This is probably related to #59.