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. 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.