Abhiroop Sarkar

The issue seems to be at the `idris-load-file` method (https://github.com/idris-hackers/idris-mode/blob/0a5a165a0dd7be7bbc4f5c9533dc21acfc811a4e/idris-commands.el#L177). Because the `idris-type-at-point` binding returns the correct applied result as well.

The WASM 2.0 spec was announced since this discussion. The changelog between version 1 and version 2 can be found here - https://www.w3.org/TR/wasm-core-2/appendix/changes.html This might be useful for someone interested...

Now when I do `ghc -O2 -optl-fuse-ld=gold -optl-static -shared -flink-rts -fPIC -o libEval.so Eval.hs hsbracket.o` (not the use of the `gold` linker) I get ``` ldd libEval.so /lib/ld-musl-x86_64.so.1 (0x7fabb8e96000) libgmp.so.10...

@TravisCardwell Thanks for looking into it. One thing I noticed is that when building GHC if it is configured with `--with-intree-gmp` then libgmp gets statically linked. I wonder if the...

I figured out the issue. It is with the `mainland-pretty` package which modified its directory structure and added a new module. This package depends on a particular version (0.2.7.1) of...

I am closing this PR for now, because I realised the proof is insufficient. I will reopen if I get back to the full proof.

The program is cleaner now and relies primarily on one key type-level programming feature to describe the entire specification. The computation happens at the type level of specification. The documentation...

@hwayne Hi, I didn't see any movement in this PR for over a month, so I was wondering if there is anything that I can do to help or clarify...

Thanks for your review! As you correctly spotted, the "issue" is entirely around point #1 and the consequences of changing the definition of the type family `Replicate`. It also ties...

@hwayne No hurries! I am also in the middle of several things to have the time to immediately make changes/fixes.