Marcial Gaißert

Also, while I wanted to use `infixAdd` for my first draft, resolving that Symbol in the `Context` sometimes failed, so I added `EviAdd`.

> If we absolutely have to add `EviAdd` then I would call it something like `ComposeEvidence`. Ah, yes, that's a better name.

https://github.com/effekt-lang/effekt/pull/164/commits/f85fb62a1d8a3d6657680bffab0cc3a98248403a uses `"infixAdd"` instead of `ComposeEvidence`. I'm not sure if that is preferable? Note: the current implementation would break if the type of `infixAdd` changed from `(Int, Int): Int`.

@phischu tested it on his machine and it was indeed the stack limit being reached.

I have now semi-splitted out evidence. It is still synonymous int in most places (i.e. `machine.builtins.Evidence` is `machine.Type.Evidence` etc), but can be used as if it weren't (there is a...

I think both are reasonable. I understand `Here` and `There` as the constructors of the evidence type, so `There` just says "outside of the current region" and still needs specification/proof...

After rethinking it, I changed `There` to be `1` now.

(and rebased to current `master`)

This also prevents globally set headers (`#+PROPERTY: header-args ...`, see https://orgmode.org/manual/Property-Syntax.html ) from working properly. Interestingly, interactively calling `anki-editor-export-subtree-to-html` (which is defined but never used in `anki-editor.el`) with the point...

We seem to make that assumption in lifted, too (commented assert): https://github.com/effekt-lang/effekt/blob/3099bd098962a580ed973261f9345c368345cdbb/effekt/shared/src/main/scala/effekt/lifted/Tree.scala#L197