| .. |
|
%41.agda
|
65e7b97953
[ #2604 ] Incomplete fix.
|
7 years ago |
|
%41.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
AccidentalSpacesAfterBeginCode.html
|
021406520c
[ #3505 ] Rename `agda-code` to `Agda`, add class names for pure codes
|
5 years ago |
|
AccidentalSpacesAfterBeginCode.lagda
|
d3f743c148
[ #2392 ] Added some missing LaTeX-backend test cases.
|
8 years ago |
|
AccidentalSpacesAfterBeginCode.quick.tex
|
f6580104e8
[ #2744, #2453 ] Added support for \begin{code}[hide].
|
7 years ago |
|
AccidentalSpacesAfterBeginCode.tex
|
f6580104e8
[ #2744, #2453 ] Added support for \begin{code}[hide].
|
7 years ago |
|
AccidentalSpacesBeforeEndCode.html
|
021406520c
[ #3505 ] Rename `agda-code` to `Agda`, add class names for pure codes
|
5 years ago |
|
AccidentalSpacesBeforeEndCode.lagda
|
d3f743c148
[ #2392 ] Added some missing LaTeX-backend test cases.
|
8 years ago |
|
AccidentalSpacesBeforeEndCode.quick.tex
|
08c553acdc
[ LaTeX backend ] A new variant: QuickLaTeX.
|
7 years ago |
|
AccidentalSpacesBeforeEndCode.tex
|
b00a3aaeea
[ #1832, LaTeX backend ] Optimisation: Fewer columns.
|
7 years ago |
|
EscapedTeXComment.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
EscapedTeXComment.lagda
|
d3f743c148
[ #2392 ] Added some missing LaTeX-backend test cases.
|
8 years ago |
|
EscapedTeXComment.quick.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
EscapedTeXComment.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Grapheme-clusters-with-pragma.compile
|
f21a87e5cc
Turned --count-clusters into a pragma option.
|
7 years ago |
|
Grapheme-clusters-with-pragma.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Grapheme-clusters-with-pragma.lagda.tex
|
f21a87e5cc
Turned --count-clusters into a pragma option.
|
7 years ago |
|
Grapheme-clusters-with-pragma.quick.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Grapheme-clusters-with-pragma.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Grapheme-clusters.compile
|
4b0f79cf9a
[ LaTeX backend ] Fixed an alignment issue.
|
7 years ago |
|
Grapheme-clusters.flags
|
72d5022161
Fixed #2449: Added a new flag, --count-clusters.
|
7 years ago |
|
Grapheme-clusters.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Grapheme-clusters.lagda.tex
|
17368ab983
[ LaTeX backend ] Documented a problem.
|
7 years ago |
|
Grapheme-clusters.quick.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Grapheme-clusters.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
HighlightOccurrences.agda
|
28aad32480
[ html ] Add missing data file and test input
|
4 years ago |
|
HighlightOccurrences.flags
|
28aad32480
[ html ] Add missing data file and test input
|
4 years ago |
|
HighlightOccurrences.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Indenting.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Indenting.lagda
|
7f5f64a0f7
Added an HTML test suite.
|
9 years ago |
|
Indenting.quick.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Indenting.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Indenting2.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Indenting2.lagda
|
7f5f64a0f7
Added an HTML test suite.
|
9 years ago |
|
Indenting2.quick.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Indenting2.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Indenting3.compile
|
a7e60e012e
[ LaTeX backend ] Fixed #3224. Fixed #3170.
|
6 years ago |
|
Indenting3.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Indenting3.lagda
|
d3f743c148
[ #2392 ] Added some missing LaTeX-backend test cases.
|
8 years ago |
|
Indenting3.quick.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Indenting3.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Indenting4.compile
|
a7e60e012e
[ LaTeX backend ] Fixed #3224. Fixed #3170.
|
6 years ago |
|
Indenting4.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Indenting4.lagda
|
7f5f64a0f7
Added an HTML test suite.
|
9 years ago |
|
Indenting4.quick.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Indenting4.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Indenting5.compile
|
a7e60e012e
[ LaTeX backend ] Fixed #3224. Fixed #3170.
|
6 years ago |
|
Indenting5.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Indenting5.lagda
|
7f5f64a0f7
Added an HTML test suite.
|
9 years ago |
|
Indenting5.quick.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Indenting5.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Indenting6.compile
|
a7e60e012e
[ LaTeX backend ] Fixed #3224. Fixed #3170.
|
6 years ago |
|
Indenting6.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Indenting6.lagda
|
7f5f64a0f7
Added an HTML test suite.
|
9 years ago |
|
Indenting6.quick.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Indenting6.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Indenting7.compile
|
a7e60e012e
[ LaTeX backend ] Fixed #3224. Fixed #3170.
|
6 years ago |
|
Indenting7.html
|
a1bda7bb28
Fixed #5335.
|
3 years ago |
|
Indenting7.lagda
|
24e14bdd87
[ fix-agda-whitespace ] Added `.lagda` extension.
|
8 years ago |
|
Indenting7.quick.tex
|
2d858381d8
Fixed #2733. Fixed #2740.
|
7 years ago |
|
Indenting7.tex
|
2d858381d8
Fixed #2733. Fixed #2740.
|
7 years ago |
|
IndentingContainer.compile
|
d3f743c148
[ #2392 ] Added some missing LaTeX-backend test cases.
|
8 years ago |
|
IndentingContainer.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
IndentingContainer.lagda
|
7f5f64a0f7
Added an HTML test suite.
|
9 years ago |
|
IndentingContainer.quick.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
IndentingContainer.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
InfixDeclaration.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
InfixDeclaration.lagda
|
b0931cc820
[ cosmetics ] typo: preceed --> precede
|
4 years ago |
|
InfixDeclaration.quick.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
InfixDeclaration.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Inline.compile
|
a7e60e012e
[ LaTeX backend ] Fixed #3224. Fixed #3170.
|
6 years ago |
|
Inline.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Inline.lagda.tex
|
27f3cbc2de
[ agda.sty ] Now code complains if it is given unrecognised options.
|
5 years ago |
|
Inline.quick.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Inline.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Issue1053.compile
|
a7e60e012e
[ LaTeX backend ] Fixed #3224. Fixed #3170.
|
6 years ago |
|
Issue1053.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Issue1053.lagda
|
7f5f64a0f7
Added an HTML test suite.
|
9 years ago |
|
Issue1053.quick.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Issue1053.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Issue1062.compile
|
80e58883f5
[ #2392 ] Fixed test case.
|
8 years ago |
|
Issue1062.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Issue1062.lagda
|
88dd8f1312
[ #2392 ] Added accidentally erased `\nonstopmode`.
|
8 years ago |
|
Issue1062.quick.tex
|
94cfe2ef3e
LaTeX output: preserve spaces in comments. (#5320)
|
3 years ago |
|
Issue1062.tex
|
94cfe2ef3e
LaTeX output: preserve spaces in comments. (#5320)
|
3 years ago |
|
Issue1241.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Issue1241.lagda
|
d3f743c148
[ #2392 ] Added some missing LaTeX-backend test cases.
|
8 years ago |
|
Issue1241.quick.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Issue1241.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Issue1618.compile
|
a7e60e012e
[ LaTeX backend ] Fixed #3224. Fixed #3170.
|
6 years ago |
|
Issue1618.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Issue1618.lagda
|
7f5f64a0f7
Added an HTML test suite.
|
9 years ago |
|
Issue1618.quick.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Issue1618.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Issue2019.compile
|
c4b6e482e0
[ #2019 ] Whitespace is now preserved in many cases.
|
7 years ago |
|
Issue2019.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Issue2019.lagda
|
c4b6e482e0
[ #2019 ] Whitespace is now preserved in many cases.
|
7 years ago |
|
Issue2019.quick.tex
|
94cfe2ef3e
LaTeX output: preserve spaces in comments. (#5320)
|
3 years ago |
|
Issue2019.tex
|
94cfe2ef3e
LaTeX output: preserve spaces in comments. (#5320)
|
3 years ago |
|
Issue2077-1.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Issue2077-1.lagda
|
6e178da7c7
[ fixed #2077 ] Regression in parsing literate files
|
8 years ago |
|
Issue2077-1.quick.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Issue2077-1.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Issue2077-2.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Issue2077-2.lagda
|
6e178da7c7
[ fixed #2077 ] Regression in parsing literate files
|
8 years ago |
|
Issue2077-2.quick.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Issue2077-2.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Issue2400-1.html
|
021406520c
[ #3505 ] Rename `agda-code` to `Agda`, add class names for pure codes
|
5 years ago |
|
Issue2400-1.lagda
|
6a79d76875
[ test ] Issue #2400
|
7 years ago |
|
Issue2400-1.quick.tex
|
6a79d76875
[ test ] Issue #2400
|
7 years ago |
|
Issue2400-1.tex
|
6a79d76875
[ test ] Issue #2400
|
7 years ago |
|
Issue2401.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Issue2401.lagda.tex
|
b40c637122
[ #2401 ] Added a test case.
|
7 years ago |
|
Issue2401.quick.tex
|
94cfe2ef3e
LaTeX output: preserve spaces in comments. (#5320)
|
3 years ago |
|
Issue2401.tex
|
94cfe2ef3e
LaTeX output: preserve spaces in comments. (#5320)
|
3 years ago |
|
Issue2445.compile
|
8c933841a5
A test case for #2445.
|
7 years ago |
|
Issue2445.html
|
021406520c
[ #3505 ] Rename `agda-code` to `Agda`, add class names for pure codes
|
5 years ago |
|
Issue2445.lagda.tex
|
8c933841a5
A test case for #2445.
|
7 years ago |
|
Issue2445.quick.tex
|
e633d11c0d
Underscores are now typeset using \AgdaUnderscore{}.
|
6 years ago |
|
Issue2445.tex
|
e633d11c0d
Underscores are now typeset using \AgdaUnderscore{}.
|
6 years ago |
|
Issue2474-2.html
|
021406520c
[ #3505 ] Rename `agda-code` to `Agda`, add class names for pure codes
|
5 years ago |
|
Issue2474-2.lagda
|
9df4026c09
[ #2474 ] Support for warning highlighting
|
6 years ago |
|
Issue2474-2.quick.tex
|
9df4026c09
[ #2474 ] Support for warning highlighting
|
6 years ago |
|
Issue2474-2.tex
|
9df4026c09
[ #2474 ] Support for warning highlighting
|
6 years ago |
|
Issue2474.compile
|
a7e60e012e
[ LaTeX backend ] Fixed #3224. Fixed #3170.
|
6 years ago |
|
Issue2474.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Issue2474.lagda
|
9df4026c09
[ #2474 ] Support for warning highlighting
|
6 years ago |
|
Issue2474.quick.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Issue2474.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Issue2536.compile
|
a7e60e012e
[ LaTeX backend ] Fixed #3224. Fixed #3170.
|
6 years ago |
|
Issue2536.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Issue2536.lagda
|
99d34e9aab
[ #2536 ] Use `Agda.Utils.IO.UTF8.readTextFile` for literate files.
|
7 years ago |
|
Issue2536.quick.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Issue2536.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Issue2588.html
|
6e4fb9d0be
[ fix #5398 ] by WYSIWYG for block comments
|
3 years ago |
|
Issue2588.lagda
|
6e4fb9d0be
[ fix #5398 ] by WYSIWYG for block comments
|
3 years ago |
|
Issue2588.quick.tex
|
6e4fb9d0be
[ fix #5398 ] by WYSIWYG for block comments
|
3 years ago |
|
Issue2588.tex
|
6e4fb9d0be
[ fix #5398 ] by WYSIWYG for block comments
|
3 years ago |
|
Issue2604.agda
|
971864fb86
[ #2604 ] Extended a test case.
|
7 years ago |
|
Issue2604.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Issue2623.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Issue2623.lagda.tex
|
9a93450c37
AgdaSuppressSpace and AgdaMultiCode no longer take an argument.
|
7 years ago |
|
Issue2623.quick.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Issue2623.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Issue2733-1.compile
|
2d858381d8
Fixed #2733. Fixed #2740.
|
7 years ago |
|
Issue2733-1.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Issue2733-1.lagda.tex
|
2d858381d8
Fixed #2733. Fixed #2740.
|
7 years ago |
|
Issue2733-1.quick.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Issue2733-1.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Issue2733-2.compile
|
2d858381d8
Fixed #2733. Fixed #2740.
|
7 years ago |
|
Issue2733-2.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Issue2733-2.lagda.tex
|
2d858381d8
Fixed #2733. Fixed #2740.
|
7 years ago |
|
Issue2733-2.quick.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Issue2733-2.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Issue2734.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Issue2734.lagda.tex
|
9b16110faa
[ #2734 test ] replace acmart with article documentclass
|
7 years ago |
|
Issue2734.quick.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Issue2734.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Issue2740-1.compile
|
2d858381d8
Fixed #2733. Fixed #2740.
|
7 years ago |
|
Issue2740-1.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Issue2740-1.lagda.tex
|
2d858381d8
Fixed #2733. Fixed #2740.
|
7 years ago |
|
Issue2740-1.quick.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Issue2740-1.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Issue2740-2.compile
|
2d858381d8
Fixed #2733. Fixed #2740.
|
7 years ago |
|
Issue2740-2.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Issue2740-2.lagda.tex
|
2d858381d8
Fixed #2733. Fixed #2740.
|
7 years ago |
|
Issue2740-2.quick.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Issue2740-2.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Issue2744.compile
|
a7e60e012e
[ LaTeX backend ] Fixed #3224. Fixed #3170.
|
6 years ago |
|
Issue2744.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Issue2744.lagda.tex
|
9a93450c37
AgdaSuppressSpace and AgdaMultiCode no longer take an argument.
|
7 years ago |
|
Issue2744.quick.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Issue2744.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Issue2756.agda
|
fbdef7c2a4
[ #2756 ] Test case.
|
6 years ago |
|
Issue2756.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Issue3020.agda
|
22808f82bb
Fixed #3020.
|
6 years ago |
|
Issue3020.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Issue3112.compile
|
b3c27b5ea4
[ fix #3112 ] separate highlighting aspect for generalized variables
|
5 years ago |
|
Issue3112.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Issue3112.lagda
|
b3c27b5ea4
[ fix #3112 ] separate highlighting aspect for generalized variables
|
5 years ago |
|
Issue3112.quick.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Issue3112.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Issue3322.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Issue3322.lagda
|
0bd190a86a
[ fixed #3322 ] For quicklatex, we need highlighting of record fields from scope checker
|
6 years ago |
|
Issue3322.quick.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Issue3322.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Issue3965.agda
|
373c88039f
[ fix #3965 ] Highlight unreachable clauses separately (#3969)
|
5 years ago |
|
Issue3965.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Issue3989.agda
|
29b629d1ba
[ #3989 ] A new OtherAspect: ShadowingInTelescope.
|
4 years ago |
|
Issue3989.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Issue4580NegativeLiterals.agda
|
a6ae585650
[ fixed #4580 ] Highlighting for FROMNAT, FROMNEG, FROMSTRING
|
4 years ago |
|
Issue4580NegativeLiterals.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Issue5043-2.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Issue5043-2.lagda.tex
|
06e4e4eacd
[ fix #5043 ] Add Hole Aspect (#5050)
|
4 years ago |
|
Issue5043-2.quick.tex
|
06e4e4eacd
[ fix #5043 ] Add Hole Aspect (#5050)
|
4 years ago |
|
Issue5043-2.tex
|
06e4e4eacd
[ fix #5043 ] Add Hole Aspect (#5050)
|
4 years ago |
|
Issue5043.agda
|
06e4e4eacd
[ fix #5043 ] Add Hole Aspect (#5050)
|
4 years ago |
|
Issue5043.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Issue982.compile
|
a7e60e012e
[ LaTeX backend ] Fixed #3224. Fixed #3170.
|
6 years ago |
|
Issue982.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Issue982.lagda
|
a7e60e012e
[ LaTeX backend ] Fixed #3224. Fixed #3170.
|
6 years ago |
|
Issue982.quick.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Issue982.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
LaTeX-succeed.compile
|
a7e60e012e
[ LaTeX backend ] Fixed #3224. Fixed #3170.
|
6 years ago |
|
LaTeX-succeed.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
LaTeX-succeed.lagda
|
6640e35882
[ #3024 ] Status quo of projection pattern in agda --latex.
|
6 years ago |
|
LaTeX-succeed.quick.tex
|
94cfe2ef3e
LaTeX output: preserve spaces in comments. (#5320)
|
3 years ago |
|
LaTeX-succeed.tex
|
94cfe2ef3e
LaTeX output: preserve spaces in comments. (#5320)
|
3 years ago |
|
Legacy-AgdaIndent.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Legacy-AgdaIndent.lagda.tex
|
b84ab4ecdf
[ LaTeX backend ] \AgdaIndent no longer takes an argument.
|
7 years ago |
|
Legacy-AgdaIndent.quick.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Legacy-AgdaIndent.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Less-extra-indentation.compile
|
1a7f6111ca
[ #3320 ] A partial fix.
|
6 years ago |
|
Less-extra-indentation.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Less-extra-indentation.lagda.tex
|
1a7f6111ca
[ #3320 ] A partial fix.
|
6 years ago |
|
Less-extra-indentation.quick.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Less-extra-indentation.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Links.compile
|
a7e60e012e
[ LaTeX backend ] Fixed #3224. Fixed #3170.
|
6 years ago |
|
Links.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Links.lagda
|
7f5f64a0f7
Added an HTML test suite.
|
9 years ago |
|
Links.quick.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Links.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
MdDontHighlightCode.flags
|
30dcb47670
[ #3366 ] Add tests
|
6 years ago |
|
MdDontHighlightCode.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
MdDontHighlightCode.lagda.md
|
3185db9f8a
Fix #5581: allow tabs in literate parts of .lagda files
|
3 years ago |
|
MdHighlightCode.flags
|
30dcb47670
[ #3366 ] Add tests
|
6 years ago |
|
MdHighlightCode.html
|
d31b47d080
[ test ] Fix
|
6 years ago |
|
MdHighlightCode.lagda.md
|
014ea684be
[ test ] Fix typo
|
6 years ago |
|
MdHighlightCode.md
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
MdHighlightCodeAuto.flags
|
30dcb47670
[ #3366 ] Add tests
|
6 years ago |
|
MdHighlightCodeAuto.lagda.md
|
30dcb47670
[ #3366 ] Add tests
|
6 years ago |
|
MdHighlightCodeAuto.md
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
MdJustHighlightAgdaAsHtml.agda
|
8330043dcb
[ fixed #3432 ] by querying also stPatternSyns in nameKinds
|
4 years ago |
|
MdJustHighlightAgdaAsHtml.flags
|
30dcb47670
[ #3366 ] Add tests
|
6 years ago |
|
MdJustHighlightAgdaAsHtml.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
MdMultiLanguage.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
MdMultiLanguage.lagda.md
|
b8df80ae48
[ literate ] Changelog, fixes for Markdown support
|
8 years ago |
|
MdOneLine.html
|
021406520c
[ #3505 ] Rename `agda-code` to `Agda`, add class names for pure codes
|
5 years ago |
|
MdOneLine.lagda.md
|
a9c3fb3972
Add Markdown support for literate Agda.
|
8 years ago |
|
MdQuotedDelim.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
MdQuotedDelim.lagda.md
|
a9c3fb3972
Add Markdown support for literate Agda.
|
8 years ago |
|
Multiline.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Multiline.lagda
|
db474668d3
[ #2304 ] Data.String isn't in scope during tests
|
8 years ago |
|
Multiline.quick.tex
|
2d858381d8
Fixed #2733. Fixed #2740.
|
7 years ago |
|
Multiline.tex
|
2d858381d8
Fixed #2733. Fixed #2740.
|
7 years ago |
|
NoNewLinesVsNewLines.html
|
021406520c
[ #3505 ] Rename `agda-code` to `Agda`, add class names for pure codes
|
5 years ago |
|
NoNewLinesVsNewLines.lagda
|
d3f743c148
[ #2392 ] Added some missing LaTeX-backend test cases.
|
8 years ago |
|
NoNewLinesVsNewLines.quick.tex
|
08c553acdc
[ LaTeX backend ] A new variant: QuickLaTeX.
|
7 years ago |
|
NoNewLinesVsNewLines.tex
|
b00a3aaeea
[ #1832, LaTeX backend ] Optimisation: Fewer columns.
|
7 years ago |
|
Number.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Number.lagda.tex
|
ceb012606a
[ agda.sty ] A new option for the code environment: number.
|
5 years ago |
|
Number.quick.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Number.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
OneSpaceIndent.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
OneSpaceIndent.lagda
|
7f5f64a0f7
Added an HTML test suite.
|
9 years ago |
|
OneSpaceIndent.quick.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
OneSpaceIndent.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Options.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Options.lagda
|
351cc32afe
[ #2452 ] More highlighting for and better typesetting of pragmas.
|
6 years ago |
|
Options.quick.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Options.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Org.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Org.lagda.org
|
cda050c1e2
[ new ] Add support for compiling literate Org documents (#3548)
|
5 years ago |
|
OrgHighlightCode.flags
|
bb6ec6a1ce
wrap org-mode exported html as html (#4552)
|
4 years ago |
|
OrgHighlightCode.lagda.org
|
bb6ec6a1ce
wrap org-mode exported html as html (#4552)
|
4 years ago |
|
OrgHighlightCode.org
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
OrgHighlightCodeAuto.flags
|
bb6ec6a1ce
wrap org-mode exported html as html (#4552)
|
4 years ago |
|
OrgHighlightCodeAuto.lagda.org
|
bb6ec6a1ce
wrap org-mode exported html as html (#4552)
|
4 years ago |
|
OrgHighlightCodeAuto.org
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
OrgMultipleLanguages.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
OrgMultipleLanguages.lagda.org
|
cda050c1e2
[ new ] Add support for compiling literate Org documents (#3548)
|
5 years ago |
|
OrgTangle.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
OrgTangle.lagda.org
|
cda050c1e2
[ new ] Add support for compiling literate Org documents (#3548)
|
5 years ago |
|
PatternSynonyms.compile
|
a7e60e012e
[ LaTeX backend ] Fixed #3224. Fixed #3170.
|
6 years ago |
|
PatternSynonyms.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
PatternSynonyms.lagda
|
8330043dcb
[ fixed #3432 ] by querying also stPatternSyns in nameKinds
|
4 years ago |
|
PatternSynonyms.quick.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
PatternSynonyms.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
PatternSynonyms2.compile
|
a7e60e012e
[ LaTeX backend ] Fixed #3224. Fixed #3170.
|
6 years ago |
|
PatternSynonyms2.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
PatternSynonyms2.lagda
|
24e14bdd87
[ fix-agda-whitespace ] Added `.lagda` extension.
|
8 years ago |
|
PatternSynonyms2.quick.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
PatternSynonyms2.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
PatternSynonyms3.compile
|
a7e60e012e
[ LaTeX backend ] Fixed #3224. Fixed #3170.
|
6 years ago |
|
PatternSynonyms3.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
PatternSynonyms3.lagda
|
24e14bdd87
[ fix-agda-whitespace ] Added `.lagda` extension.
|
8 years ago |
|
PatternSynonyms3.quick.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
PatternSynonyms3.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
QuickLaTeX.compile
|
a7e60e012e
[ LaTeX backend ] Fixed #3224. Fixed #3170.
|
6 years ago |
|
QuickLaTeX.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
QuickLaTeX.lagda.tex
|
fa09a8fe74
[ re #4908 ] add explicit --sized-types flag to test suite
|
3 years ago |
|
QuickLaTeX.quick.tex
|
fa09a8fe74
[ re #4908 ] add explicit --sized-types flag to test suite
|
3 years ago |
|
QuickLaTeX.tex
|
fa09a8fe74
[ re #4908 ] add explicit --sized-types flag to test suite
|
3 years ago |
|
Relative-indentation.compile
|
7e36b92919
[ #1832, LaTeX backend ] Indentation is handled differently.
|
7 years ago |
|
Relative-indentation.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Relative-indentation.lagda.tex
|
9a93450c37
AgdaSuppressSpace and AgdaMultiCode no longer take an argument.
|
7 years ago |
|
Relative-indentation.quick.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Relative-indentation.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
RsTHighlightCode.flags
|
2d980891f5
[ close #3373 ] Implement the proposed feature (#3384)
|
6 years ago |
|
RsTHighlightCode.lagda.rst
|
e205a43e87
Fixed #1209.
|
6 years ago |
|
RsTHighlightCode.rst
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
RsTHighlightCodeAuto.flags
|
2d980891f5
[ close #3373 ] Implement the proposed feature (#3384)
|
6 years ago |
|
RsTHighlightCodeAuto.lagda.rst
|
fa09a8fe74
[ re #4908 ] add explicit --sized-types flag to test suite
|
3 years ago |
|
RsTHighlightCodeAuto.rst
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
RsTQuotedDelim.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
RsTQuotedDelim.lagda.rst
|
8d6b5cb2d0
Add documentation tests
|
8 years ago |
|
Tag.compile
|
7f5f64a0f7
Added an HTML test suite.
|
9 years ago |
|
Tag.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Tag.lagda
|
7f5f64a0f7
Added an HTML test suite.
|
9 years ago |
|
Tag.quick.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Tag.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
TeXExtension.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
TeXExtension.lagda.tex
|
d3f743c148
[ #2392 ] Added some missing LaTeX-backend test cases.
|
8 years ago |
|
TeXExtension.quick.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
TeXExtension.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
ThreeNewLines.html
|
021406520c
[ #3505 ] Rename `agda-code` to `Agda`, add class names for pure codes
|
5 years ago |
|
ThreeNewLines.lagda
|
d3f743c148
[ #2392 ] Added some missing LaTeX-backend test cases.
|
8 years ago |
|
ThreeNewLines.quick.tex
|
6cb0366e8c
Fixed #2734.
|
7 years ago |
|
ThreeNewLines.tex
|
6cb0366e8c
Fixed #2734.
|
7 years ago |
|
Trailing-whitespace.compile
|
4ce1d6ff3b
[ LaTeX backend ] Small change to the treatment of trailing whitespace.
|
7 years ago |
|
Trailing-whitespace.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
Trailing-whitespace.lagda.tex
|
44ec9bf03c
[ LaTeX backend ] Small change to the treatment of trailing whitespace.
|
7 years ago |
|
Trailing-whitespace.quick.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Trailing-whitespace.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
TrailingColon.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
TrailingColon.lagda.rst
|
8d6b5cb2d0
Add documentation tests
|
8 years ago |
|
UnicodeInput.compile
|
7f5f64a0f7
Added an HTML test suite.
|
9 years ago |
|
UnicodeInput.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
UnicodeInput.lagda
|
7f5f64a0f7
Added an HTML test suite.
|
9 years ago |
|
UnicodeInput.quick.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
UnicodeInput.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
ltgt.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
|
ltgt.lagda
|
e7da0ceab6
[ fix ] < and > need to be in math mode in latex (#3370)
|
6 years ago |
|
ltgt.quick.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
ltgt.tex
|
55c22499cc
[ #4093 ] Update LaTeX and HTML test output
|
4 years ago |
|
Σ.agda
|
65e7b97953
[ #2604 ] Incomplete fix.
|
7 years ago |
|
Σ.html
|
edd8334381
[ #5427 ] Removed support for subtyping for erasure and irrelevance.
|
3 years ago |
Nils Anders Danielsson