Miëtek Bak
Miëtek Bak
Could we have some clarifying comments added to the stdlib about the definition of surjection actually being the definition of split surjection? It would be helpful to people such as...
Syntax rules using symbols as separators require more parentheses than syntax rules using keywords as separators. Tested with Idris 0.9.19. ``` idris module SyntaxProblem helper : () -> () ->...
Adding quotes to syntax rules sometimes appears to confuse the parser. Tested with Idris 0.9.18.1. #### No quotes This works: ``` idris module NoProblem foo' : Unit -> (Unit ->...
Contexts for goals within a `with` clause are printed without making use of a `DISPLAY` rule that is used elsewhere. This is Agda 2.5.4.2. ```agda module DisplayBug where open import...
Let’s say we are reorganising a repository, and we rename the file “Foo.agda” to “Bar.agda”, in the filesystem. Next, we update “Everything.agda” to `import Bar`, and we reload the file....
### Implementations - [x] M. Łach (1998) ### Literature - [ ] Z. Spławski (1988) “Teoriodowodowe podejście do programów funkcyjnych i typów danych”, report, Raporty Centr. Oblicz. PWr. 1988, Ser....
I’d like to use `Data.List.Any` from the standard library _and_ have readable goals. I tried the following, but was rebuked: ``` agda {-# DISPLAY Any (_≡_ x) Y = x...
We currently have the ability to fix the name of the Haskell function to which the GHC backend automatically translates an Agda function. ```agda module Analogy where open import Agda.Builtin.Nat...
As discussed with @andreasabel and @jespercockx at AIM XL. ```agda module Bug where data A : Set where data B : Set where data C : A → B →...
As discussed with @andreasabel, @UlfNorell, and @plt-amy at AIM XL. ```agda module Bug where module Works where data LibraryType : Set where foo : LibraryType data UserType : Set where...