Zoe Stafford

Are you using an up to date version of idris2? That file `build.idr` requires the escaped form of the `system` function which was added to base, I think fairly recently.

@csabahruska Passing too and from FFI functions. My current use case is arbitrary precision integers in the idris2-grin backend. @luc-tielen unfortunately not all C libraries are idiomatic.

In the long term, yes (eg for `IORef`) however I don't think for `Integer` all that is needed is a static (as in known at runtime) finaliser function (which can...

Actually, the grin optimiser inlines apply and eval before anything else, so this isn't really an issue. I just need to turn off the inlining optimisation in my idris2 grin...

I don't have time to fix this right now, so I'll revert it and let someone else work on it.

Reverting the commit now, I'll make sure to check with pack when I get round to fixing it

I'm currently on holiday, so for the next few days I'm unable to do basically anything other than comment or merge, so I'm more than happy to leave this to...

You need to add the test to `tests/Main.idr` for it to actually run. Edit: I would suggest adding a new `TestPool`, eg using `testsInDir`

Do you know which recursive function is the problem? I can have a go at fixing it

I've found it I think: `rulebook::sanitize_rule::sanitize_term`, I can make this tail recursive using CPS if that's ok?