blob: 82df2656e62ec7453669189e97fefe665e3f1d63 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
|
B: A New Way of Looking at the Agda Standard Library
====================================================
B (as in ‘Plan B’) is an compatible extension of the [Agda standard library][]
intended to support general programming with dependent types. Its goal is to
eliminate the large numbers of imports common in Agda programs through universal
use of type classes and pre-imported names.
B fulfils a different role than the [Agda Prelude][]. The Agda Prelude is a
fully-featured standard library alternative, but it comes at the expense of
compatibility. The Prelude is also heavily programming-oriented, disabling the
termination checker when appropriate. B, on the other hand, takes a more
general route: it is much smaller, makes only compatible extensions to the
standard library, and it avoids turning off the termination checker.
Getting started
---------------
B is probably not yet ready for general use. However, if you’d like to try it,
you should probably use [Agda][] v2.4.2.2 and version 0.9 of the standard
library.
Copyright and licence
---------------------
B is copyright © 2015 [Benjamin Barenblat][] and licensed under the
[Apache License, version 2.0] [Apache License]. Unless required by applicable
law or agreed to in writing, B is distributed on an _‘as is’ basis, without
warranties or conditions of any kind_, either express or implied. See the
License for the specific language governing permissions and limitations under
the License.
[Agda]: http://wiki.portal.chalmers.se/agda/
[Agda Prelude]: https://github.com/UlfNorell/agda-prelude
[Agda standard library]: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary
[Apache License]: http://www.apache.org/licenses/LICENSE-2.0
[Benjamin Barenblat]: https://benjamin.barenblat.name/
|
