Alex Gryzlov
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.