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