Alexander Bentkamp
Alexander Bentkamp
My stuff doesn't work with lambdas, but if you replace ``` def f : a -> a := fun x. x. def g : a -> a := fun x....
I thought we might want to interpret the clause `a
I've adapted the grammar and pushed it directly to `master`. I've tried a couple of problems from the TIP library and they can be parsed now. Let me know if...
I've fixed the parsing issue and pushed it to `master`. The `ApplyError` is more difficult to fix. The issue is a clash of variable names in the induction module and...
I don't know how large the impact is on heuristics, but I saw that it confused @petarvukmirovic who wrote an assertion `assert((C.proof_depth c)
I don't know if Avatar really needs it's own kind of step because if `ϕ
What do you mean by "refines inference"? Right now it looks like this: ``` type kind = | Intro of source * role | Inference of rule * tag list...
Sorry for the late reaction. Could you create a pull request? I'd be happy to merge it. I assume the `assert false` is there because an empty clause would usually...
Essentially all of the contents of this pull request have already been added independently now.
There are a couple of restrictions of emscripten pthreads listed here, which might cause this: https://emscripten.org/docs/porting/pthreads.html Unfortunately, I dont think I will have the time to look into this in...