Andreas Abel
Andreas Abel
Here is a version without the standard library: ```agda \documentclass{article} \usepackage{agda} \begin{document} \begin{AgdaMultiCode} \begin{code} case_of_ : {A B : Set} (a : A) (f : A → B) → B...
Shrank the generated latex file to this: ```tex \documentclass{article} \usepackage{agda} \begin{document} \begin{AgdaMultiCode} %% The column names must be different, e.g foo/bar/baz \begin{code} \\ %% needed \>[foo] \end{code} \begin{code} \>[bar] \end{code}...
Shrinking away `agda.sty` I arrive at this `polytable` reproducer (still same error): ```latex \documentclass{article} \RequirePackage{polytable} \defaultcolumn{l} \begin{document} %% The column names must be different \begin{pboxed}\savecolumns \\ %% needed \>[foo] \end{pboxed}...
This might be an issue in `polytable` rather than in `agda.sty`. I reported this upstream: - https://github.com/kosmikus/lhs2tex/issues/104
This is an upstream bug, and we have issued a prayer; the gods will fix it or not. No need to be on the milestone for 2.7.
When I see `open public` in a parametrised module, I see red. It has a weird semantics I do not agree with.
Regression in 2.5.2 smells like a _parameter refinement_ issue. Bisecting with: - GHC 7.10.3 - Cabal 2.4.1 - Happy 1.19.5 ``` agda-bisect-v1 -w ghc-7.10.3 --with-cabal=cabal-2.4.1 --good v2.5.1.1 --bad v2.5.2 --must-fail...
Actually bisection was just a wild goose chase. The only difference from 2.5.1 to 2.5.2 is that the `R` argument to `s` changed from visible to hidden, making the OP...
This may point to a systematic problem of `hlint`: it suggests mathematically correct refactorings, but code has two consumers, the compiler, and the human reader, and a refactoring must be...