 Fredrik Nordvall Forsberg
|
a50ff581f3
[ #2487 ] consistency checking of options
|
6 роки тому |
 Ulf Norell
|
a751e811a8
[ test ] use Agda.Builtin.* in test/Common
|
9 роки тому |
 Andreas Abel
|
666c99c3b0
Merge branch 'maint-2.4'
|
9 роки тому |
|
Andreas Abel
|
6243a9136f
[ testsuite ] Added Common.Maybe, also to Prelude.
|
9 роки тому |
|
Ulf Norell
|
a431535220
[ reflection ] added builtins for the unit type
|
9 роки тому |
 Philipp Hausmann
|
de5bf1989a
[ tests ] Merge "Common" with backend tests "Prelude".
|
10 роки тому |
 Nils Anders Danielsson
|
d226fdca6e
[ test suite ] Made if_then_else_ more general.
|
10 роки тому |
|
Andreas Abel
|
ef4d57695a
[ testsuite ] Moved _*_ to Common.Prelude.
|
10 роки тому |
|
Andreas Abel
|
1b14484b23
Added if_then_else_ to test/Common/Prelude.agda.
|
11 роки тому |
|
Andreas Abel
|
063b8941d6
Added _++_ to test/Common/Prelude.agda.
|
11 роки тому |
|
Andreas Abel
|
1fc79b89ce
Added empty type, unit type, and predecessor to Common.Prelude.
|
11 роки тому |
 ulfn
|
d05260528c
[ issue 730 ] BUILTIN NATURAL now binds ZERO and SUC
|
11 роки тому |
|
Andreas Abel
|
9b647b76f3
Now Agda.Prim contains the level primitives and is automatically imported.
|
11 роки тому |
|
andreas.abel
|
aa0a0f463c
Big refactoring: internal syntax in spine form.
|
11 роки тому |
|
Andreas Abel
|
fe680e125e
Added more types and compiled pragmas to Common.Prelude.
|
12 роки тому |
 ajeffrey
|
75d659af6c
JSOptimizableFFI
|
13 роки тому |
|
ajeffrey
|
4e0c7d8a1c
JSFFI
|
13 роки тому |
 Nicolas Pouillard
|
037459a8ff
Add support for term unquoting
|
14 роки тому |
|
Nicolas Pouillard
|
ab74bb4afe
Move test/succeed/Common to test/Common. This will allow fail/ to use it as well.
|
14 роки тому |
