Hoshino Tented
Hoshino Tented
In Eta, this code `matchRegexAll (mkRegex "[0-9]+") "123"` returns `Just ("","123","",[])`. But in GHCi, the same code returns `Just ("","123","",["123"])`. I was using regex-compat with version "0.95.1".
The goals of this PR are: + [ ] Configurable LSP options + [ ] Rendering Doc by using LSP options instead of `debugRender()`
Aya version: `Aya 0.30-SNAPSHOT (9134503de233dad58f12e83920d9445829542578)` Code: ```aya > open data Nat | O | S Nat data Nat : Type 0 | O | S (_5 : Nat) > :{...
Let Term
+ [x] `Let Term` and normalization + [x] `Nested` interface for nested structure + [x] `LetPrettier` for prettying let-like things TODO: + [ ] rendering the type of the bind...
```aya open data Wrapper (P : Type) | wrap (P -> False) def what? (m : Nat) : Wrapper (suc m = 0) => wrap (\ x => z≠s (sym...
Assume that: * A library `A`, which defines `prim I` * A library `B`, which depends on library `A` and defines nothing. * A library `C`, which depends on library...
https://github.com/JetBrains/Arend/pull/199 Feature write de good, next second is mine.
I think we need a highlight configuration for GitHub, I found something from [here](https://docs.github.com/en/get-started/writing-on-github/working-with-advanced-formatting/creating-and-highlighting-code-blocks)
* `Inf` ops * `NaN` ops