Alex Gryzlov

@ecavallo yeah, those are basically paths^1 between `A→unit` and `unit→A` defined by univalence

@ecavallo Oh wow, I have been using that exact term and didn't realize the path types are wrong!!! Thanks!

What about simply reusing the `=` syntax: `\{x=y} => ...`, and have `\{x=x} ~ \{x}`?

Yeah, this is why I suggested the `\{i=j}` renaming syntax. It's kind of orthogonal to the positionality but solves a similar issue.

I'm currently doing the integers `mod 2^n` @`idris-bi` to express proofs for functions on machine bytes, which seems to be sufficient to translate the current version of this library -...

https://github.com/reactormonk/non-constant-memory/pull/1 describes one way to profile Haskell code

@jutaro The workaround I've settled on for now is to only use the syntax highlighting and check the holes in REPL in the terminal panel. Of course you lose case...

> Apparently an implementation cannot mention a universally quantified variable standing for a value. All the arguments have to be either types or constructors... Yeah, that's a known limitation in...

I don't think so, `BoxedParser` would evaluate to a lambda and cause the exact same error :( I've just discovered though, that you can in fact inline the helper -...

Yeah, writing `map {a=Parser _ _ _ _} nelist rec` works! I'm using 4 params here since the project using this is still based on the `master` branch.