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