Marc Petit-Huguenin
Marc Petit-Huguenin
Notes: - I left Make Lemma alone, as it can be lifted as a top-level function or as a local (where clause) function, but the indentation would be different. -...
This is a corner case, but an annoying one when migrating idris1 files to literate idris2 files. # Steps to Reproduce Crete two files with the same name, different content,...
When using AddClause on an interface implementation, the operator clauses are invalid. See also #248 and #247 # Steps to Reproduce Loading the following in the REPL and executing ":ac...
AddClause on an interface implementati9on should add all the clauses. See also #247. Loading the following in the REPL and executing ":ac 4 Show" ``` data Blah : Type where...
When using AddClause on an interface implementation, the clause should be indented. # Steps to Reproduce Loading the following in the REPL and executing ":ac 4 Show" ``` data Blah...
**Describe the bug** "HTTP and Web Services" described in chapter 4 of the packages manual does not seem to exist in the officially released installer. **To Reproduce** ergo> 'http://example.com'[http->(?r, ?w)]@\http....
**Describe the bug** When loading a JSON file that contains strings with single quote (section 1.3 of "A Guide to ERGOAI Packages"), the quote is not escaped. **To Reproduce** //...
I extended idris2-dom with the Types/Prims API for WebRTC, but now I am stuck because many of the APIs are returning a Promise. Actually the first API where I encounter...