Naïm Camille Favier
Naïm Camille Favier
Closes https://github.com/NixOS/nixos-search/issues/535, closes https://github.com/NixOS/nixos-search/issues/525 To do: - [x] We're currently creating a new temporary file containing the xref lua filter for *each* Pandoc invocation. This is bad. I think it...
Fixes https://github.com/NixOS/nixos-search/issues/537 maybe.
> `Checking Foo (/path/to/Foo.agda).\n` Started appearing after upgrading from 0.4.4 to 0.4.7.
4.1.0 [fails](https://github.com/NixOS/nixpkgs/pull/261174) to build on x86_64-darwin with the following log: https://gist.github.com/ncfavier/74654ee232fe4c5b20fabdc85b3e2012#file-4-1-0-fail-txt. Also included in that gist is the full build log for 4.0.5. Notice in particular the following diff: ```diff...
The `go` package in nixpkgs looks like this: ``` lrwxrwxrwx 1 root root 12 Jan 1 1970 bin -> share/go/bin dr-xr-xr-x 3 root root 4.0K Jan 1 1970 share ```...
Since debug printing was made optional in https://github.com/agda/agda/pull/6863, the test suite needs to be run with `make install-bin-debug test`. This should either be clarified in the documentation, or `test` should...
Forked from https://github.com/agda/agda/issues/6009#issuecomment-1501781092 @jespercockx says: > I think using coerce here actually more sensible than equalType, since it will also work with subtyping (e.g. --sized-types or --cumulativity).
Forked from https://github.com/agda/agda/issues/6009#issuecomment-1501781092 @jespercockx says: > I don't see any immediate negative effects of doing this, but I'd want to check with @UlfNorell or @andreasabel first. We did have some...
I am trying to generate something like the following function using reflection: ```agda data Unit : Set where unit : Unit rec : ∀ {A : Set} (a : A)...
```agda open import Agda.Builtin.Equality id : {A : Set} → A → A id x = x infixr 9 _∘_ _∘_ : {A B C : Set} → (B →...