Xia Li-yao
Xia Li-yao
The following snippet ```coq Reserved Notation " t '-->' t' " (at level 40). Inductive step : nat -> nat -> Prop := where " t '-->' t' " :=...
I'll add more items as I think of more. ### Graph algorithms - [ ] BFS/Dijkstra (day 15) - [ ] Topological sort (day 7, though the extra constraint that...
https://github.com/andrenth/ocaml-stdint/blob/e3cc9318354d3d195b34e362e631222d284899a5/lib/stdint.ml#L696 Test case: ``` Int128.(compare (shift_right_logical (of_int (-1)) 1) zero);; (* actual: -1 *) (* expected: 1 *) ```
``` LF t : type = | c : ({x : _} t) -> t ; ``` ``` Uncaught exception. Please report this as a bug. File "src/core/index.ml", line 357,...
In `Weak_Normalization.bel`, the main proof makes the term `M` decrease, but I can incorrectly claim that it is the context `g` that's decreasing. https://github.com/Beluga-lang/Beluga/blob/1d39095c99dc255d972a339d447dc04286d8c13f/examples/literate_beluga/2Advanced/Weak_Normalization.bel#L157 i.e., Beluga accepts the `/ total...
I'm using Happy to generate `.hs` files from `.y` files, and stan reports errors in the `.hs` file (notably, Happy-generated files use `(!!)`) that I would like to exclude from...
In `feed()`, there are two places throwing exceptions: one when the lexer fails, and one when the parser fails. However both just throw an `Error()` (in particular, the former swallows...
We have an instance `(Eq1 v, Eq a) => Eq (Reference v a)` , which requires that the underlying reference type be comparable (`Eq a`). That happens to be fine...
Closes #15936 - [x] Added **changelog**. - [x] Added / updated **documentation**. - [ ] Opened **overlay** pull requests (hopefully none necessary).
Right now when I switch between projects using different Coq versions I have to remember to first do an `opam switch`. Can we tell PG which switch to use on...