diff options
author | Benjamin Barenblat <bbaren@mit.edu> | 2015-04-23 14:14:37 -0400 |
---|---|---|
committer | Benjamin Barenblat <bbaren@mit.edu> | 2015-04-23 14:14:37 -0400 |
commit | e9fbc822bd34a5f9c698f1bc018fb95db8f7123a (patch) | |
tree | ad587c78e708d66d552db328bc696c945870b2a8 /README.md | |
parent | 3db42fabef4833cb0193ce4605e43dc0254aa7b2 (diff) |
Add readme and licence
Diffstat (limited to 'README.md')
-rw-r--r-- | README.md | 37 |
1 files changed, 37 insertions, 0 deletions
diff --git a/README.md b/README.md new file mode 100644 index 0000000..82df265 --- /dev/null +++ b/README.md @@ -0,0 +1,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/ |