Łukasz Czajka

Inspecting gives: ``` Type: wasm Size: 2.1 KB Imports: Functions: Memories: Tables: Globals: Exports: Functions: "encodeBool": [I32] -> [I64] "_validate_tx": [I64, I64, I64, I64, I64, I64, I64, I64] -> [I64]...

CoqHammer was designed to work well with "standard Coq", i.e., standard-library-like developments. Poor performance on mathcomp is a known issue and an open research problem (which I personally won't work...

Thanks for submitting this! You can use `make format` to ensure that your code follows our formatting guidelines (so ormolu won't fail).

Even Agda has those without forcing the user to write the damn spaces: https://agda.readthedocs.io/en/v2.6.0.1/language/function-definitions.html#as-patterns

I opened the issue because it came up while designing the complex "Match" in the core. It's not a big deal to have as-patterns in the core, so I think...

I think this is the same issue as #1596. Partial application will be fixed with the new backend.

In general, only `MemRepConstr` is supported in C code generation. There are macros/functions in the C runtime that enable support for other representations, but they have not been tested and...

We agreed on #1638

Will be closed with a proper implementation of a pattern compilation algorithm from the literature (issue #1798).

We're using the path library.