X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fwww%2Fmatita%2Flibrary.shtml;h=3c4246f313b566485c3bf0ec9180281e0221b06b;hb=1341f9c234571b4172cd76cd84e7230039cb4642;hp=c22db5e1ce9f03802dcbcb812811ff85175bef68;hpb=ecf6f2741d56261acf4580379d35117d80385da2;p=helm.git diff --git a/helm/www/matita/library.shtml b/helm/www/matita/library.shtml index c22db5e1c..3c4246f31 100644 --- a/helm/www/matita/library.shtml +++ b/helm/www/matita/library.shtml @@ -59,8 +59,30 @@
The formal system λδ is a typed λ-calculus that + pursues the unification of terms, types, environments and contexts + as the main goal. + λδ takes some features from the Automath-related + λ-calculi and some from the pure type systems, but differs + from both in that it does not include the Π construction while it + provides for an abbreviation mechanism at the level of terms. +
+ +The development presents the proofs of some important properties that + λδ enjoys. In particular: +
- See the λδ home page. + See the λδ home page + for more information.