Domů Procházet Nápověda
Přihlásit se
caryoscelus
/
agda
Sledovat 1
Oblíbit 0
Rozštěpit 0
Soubory Úkoly 0 Pull Requesty 0 Wiki
Větev: js_amd
Větve Značky
agda
/
doc
/
user-manual
/
language
Liang-Ting Chen cde693e976 [ update ] Add a description about `formatErrorParts` před 2 roky
..
Makefile 1b0a5aff0d make: Consistently invoke make via $(MAKE) před 4 roky
abstract-definitions.lagda.rst fa09a8fe74 [ re #4908 ] add explicit --sized-types flag to test suite před 3 roky
built-ins.lagda.rst fa09a8fe74 [ re #4908 ] add explicit --sized-types flag to test suite před 3 roky
coinduction.flags b43e3ae21a Make documentation into literate Agda (I) před 8 roky
coinduction.lagda.rst f972beabcf [ doc ] minor changes před 3 roky
copatterns.lagda.rst 50542b1928 Documentation: fixes a plural issue in copatterns před 5 roky
core-language.lagda.rst 4cce39b7ae [ fix #3874 ] updated core language in user manual (#4673) před 4 roky
coverage-checking.lagda.rst bfff1de33b [ fix #3961 ] Add documentation for coverage checking před 3 roky
cubical.lagda.rst 138f578c08 [ #5601 ] Now --erased-cubical supports higher constructors. před 3 roky
cumulativity.lagda.rst 07839167e8 [ cumulativity ] Add user manual and changelog entry for cumulativity před 5 roky
data-types.lagda.rst a1ce9bf326 [ doc ] A third editing pass over 'A Taste of Agda' před 3 roky
flat.lagda.rst edd8334381 [ #5427 ] Removed support for subtyping for erasure and irrelevance. před 3 roky
foreign-function-interface.flags 94e5872200 [ user manual ] invoke the ghc backend on ffi documentation před 7 roky
foreign-function-interface.lagda.rst 62816acdd2 Merge pull request #4156 from mdimjasevic/doc-ffi-haskell-type před 5 roky
function-definitions.lagda.rst fa09a8fe74 [ re #4908 ] add explicit --sized-types flag to test suite před 3 roky
function-types.lagda.rst 8738b27862 [ docs ] fix typo, `\\` -> `\` před 3 roky
generalization-of-declared-variables.lagda.rst 6cc76903fd [ fix #5683 ] don't generalize if we're already generalizing před 3 roky
guarded-cubical.lagda.rst b4808830ff [ guarded doc ] Documented the current @tick application rule. před 3 roky
implicit-arguments.lagda.rst f46b435609 [ #3901 ] document new syntax {A} -> B and {{A}} -> B in user manual před 5 roky
index.rst 283b3d5adb [ doc #1625 ] documented `--experimental-lossy-unification` (#5690) před 3 roky
instance-arguments.lagda.rst fa09a8fe74 [ re #4908 ] add explicit --sized-types flag to test suite před 3 roky
irrelevance.lagda.rst edd8334381 [ #5427 ] Removed support for subtyping for erasure and irrelevance. před 3 roky
lambda-abstraction.flags b507471bb7 [ doc ] Converted remaining into literate files před 8 roky
lambda-abstraction.lagda.rst d6cec561d7 [ #4525 ] Erased pattern-matching lambdas. před 3 roky
let-and-where.lagda.rst fa09a8fe74 [ re #4908 ] add explicit --sized-types flag to test suite před 3 roky
lexical-structure.flags b507471bb7 [ doc ] Converted remaining into literate files před 8 roky
lexical-structure.lagda.rst ef433beed7 [ user-manual ] synced list of keywords with Lexer.x před 3 roky
literal-overloading.flags b507471bb7 [ doc ] Converted remaining into literate files před 8 roky
literal-overloading.lagda.rst 951ced3c8a [ fix #4925 ] don't use fromNat/Neg/String unless in scope unqualified před 4 roky
lossy-unification.lagda.rst 283b3d5adb [ doc #1625 ] documented `--experimental-lossy-unification` (#5690) před 3 roky
mixfix-operators.lagda.rst 2301a13c3b [ doc ] workaround for setting fixity of operators in telescopes (#5256) před 3 roky
module-system.lagda.rst fa09a8fe74 [ re #4908 ] add explicit --sized-types flag to test suite před 3 roky
mutual-recursion.lagda.rst b668e6361c [ fixed #5356 #5336 ] interleaved mutual: data _ where instead of constructor před 3 roky
pattern-synonyms.lagda.rst 77c9e4d070 [ doc ] Improved documentation of the `OPTIONS` pragma. před 5 roky
positivity-checking.lagda.rst 77c9e4d070 [ doc ] Improved documentation of the `OPTIONS` pragma. před 5 roky
postulates.lagda.rst eaf868d850 [ doc ] Port documentation of postulates from the wiki. před 6 roky
pragmas.lagda.rst da25203429 [ #4681 ] update documentation před 3 roky
prop.lagda.rst 2007630d78 Fix mistake in date of paper on Prop před 5 roky
record-types.lagda.rst d8145b921a [ #4786 ] Made parameters erased. před 3 roky
reflection.lagda.rst cde693e976 [ update ] Add a description about `formatErrorParts` před 2 roky
rewriting.lagda.rst f5a698da0d [ rewriting ] Add global confluence checker for rewrite rules před 4 roky
runtime-irrelevance.lagda.rst d8145b921a [ #4786 ] Made parameters erased. před 3 roky
safe-agda.lagda.rst f713441fc4 Extend reflection with system calls (#4759) před 4 roky
sized-types.flags efdada52ba [ fix #5352 ] new option --no-double-check for .flags file in testsuite před 3 roky
sized-types.lagda.rst fa09a8fe74 [ re #4908 ] add explicit --sized-types flag to test suite před 3 roky
sort-system.lagda.rst f713441fc4 Extend reflection with system calls (#4759) před 4 roky
syntactic-sugar.lagda.rst 61ea3a3aca Minor Typo před 4 roky
syntax-declarations.lagda.rst a3222370f2 [ #5201 ] Made syntax declarations more liberal. před 3 roky
telescopes.lagda.rst 2fbef7d4bb [ fix #1097 ] more liberal syntax in telescopes (#3884) před 5 roky
termination-checking.lagda.rst 77c9e4d070 [ doc ] Improved documentation of the `OPTIONS` pragma. před 5 roky
universe-levels.lagda.rst 5f94713332 [ fix #5313 ] documentation of level properties (#5327) před 3 roky
with-abstraction.flags b507471bb7 [ doc ] Converted remaining into literate files před 8 roky
with-abstraction.lagda.rst 0fc6b558b0 [ re #5386 ] Address two comments by @nad před 3 roky
without-k.lagda.rst e205a43e87 Fixed #1209. před 6 roky