 Andrea Vezzosi
|
283b3d5adb
[ doc #1625 ] documented `--experimental-lossy-unification` (#5690)
|
3 years ago |
 Jesper Cockx
|
dca1c55695
[ doc ] Rewriting some parts of first section of "A Taste of Agda"
|
3 years ago |
 Liang-Ting Chen
|
553af521ca
[ new ] Add a stub page for the guarded cubical mode to begin with (#5035)
|
4 years ago |
 herminie
|
73b29982d6
[ fix #4572 ] added piSort UnivSort funSort and Setω+n to the user-manual (#4645)
|
4 years ago |
 Ulf Norell
|
5fe0102358
[ fix #3855 ] document @0
|
4 years ago |
|
Jesper Cockx
|
07839167e8
[ cumulativity ] Add user manual and changelog entry for cumulativity
|
5 years ago |
|
Andrea Vezzosi
|
3b4121d35a
[ doc flat ] Flat modality documentation.
|
5 years ago |
|
Jesper Cockx
|
275efccf44
[ prop ] Add user manual + changelog
|
6 years ago |
 Peter Divianszky
|
fdd65a2a7b
add documentation for generalization of declared variables
|
6 years ago |
|
Andrea Vezzosi
|
cf2e965651
[ doc ] some docs for syntax declarations
|
7 years ago |
|
Ulf Norell
|
9a15b1cddf
Merge stable-2.5
|
7 years ago |
|
Ulf Norell
|
f6a2f10e74
[ do-notation ] user manual
|
7 years ago |
 Víctor López Juan
|
d2b0d4a160
[ doc ] Cubical documentation stub
|
7 years ago |
 Andreas Abel
|
e23c19d315
Fixed #2055: user-manual for abstract definitions
|
8 years ago |
|
Andreas Abel
|
595a8c83ab
[ doc #2081 ] turned let-expressions.rst into let-and-where.lagda.rst
|
8 years ago |
 Andrés Sicard-Ramírez
|
d74bb5b283
[ #1614, #1760 ] Added documentation.
|
9 years ago |
|
Ulf Norell
|
b93e32070d
[ doc ] with-abstraction
|
9 years ago |
|
Ulf Norell
|
99bc948806
[ doc ] finished the built-in section
|
9 years ago |
|
Ulf Norell
|
fe5ec8c00c
[ user manual ] language reference skeleton
|
9 years ago |
