X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fweb%2Fhome%2Fimplementation.ldw.xml;h=76bd89b33a94626779f64dd34c101189cb5099bd;hb=528f8ea107f689d07d060e1d31ba32bf65b4e6ba;hp=6d0237d98ee59cb6b686a070d0aa5248b3895572;hpb=58e83e119ca3829affae2851cd512748131a766b;p=helm.git diff --git a/helm/www/lambdadelta/web/home/implementation.ldw.xml b/helm/www/lambdadelta/web/home/implementation.ldw.xml index 6d0237d98..76bd89b33 100644 --- a/helm/www/lambdadelta/web/home/implementation.ldw.xml +++ b/helm/www/lambdadelta/web/home/implementation.ldw.xml @@ -3,36 +3,25 @@ Tools - λδ Digital Library (LDDL) + Open Symbolic Notation + - The λδ Digital Library is part of HELM - and contains resources expressed in the systems of the λδ family. + Open Symbolic Notation, abbreviated OSN, + is an easy and flexible data-interchange text format + intended for the lightweight representation of + generic abstract syntax trees in the domain of formal languages. + Additional information is available at OSN web site. - - - Landau's "Grundlagen der Analysis" - (from Jutting's specification in Automath). - - - - static pages (updated ), - data set (updated ), - HELM server URL (updated ). - - - - - Grundlagen's definition "t234" - in λδ version 4. - - Helena + + Helena Helena is a processor for the systems of the λδ family, @@ -75,7 +64,7 @@ (the specification language of Matita). The overall validation speed of the "Grundlagen der Analysis" increases of 34% with respect to version 0.8.1. - Documentation (J3a). + Documentation (J3a). [Svn revision: 13035] (archived source code). The specification of Landau's "Grundlagen der Analysis" @@ -127,7 +116,7 @@ Supports λδ version 2 with naive implementation of impredicative sort inclusion. Features importation from Automath and exportation to XML. - Documentation (R2a). + Documentation (R2a). [Svn revision: 10304] (archived source code). A Jed mode @@ -146,45 +135,29 @@ - Open Symbolic Notation - - Open Symbolic Notation (OSN) is an easy data-interchange textual format - based on symbolic expressions. - OSN is completely language independent but uses widely accepted conventions. - These features make OSN ideal for storing and exchanging tree-like data structures - in a lightweight manner. - + λδ Digital Library (LDDL) + - An OSN text uses the UTF-8 character set - and contains the next tokens: + The λδ Digital Library is part of HELM + and contains resources expressed in the systems of the λδ family. - - <symbol> a non-empty sequence of the 66 characters + - . 0..9 A..Z _ a..z - this sequence can represents the identifiers and the numerical constants of most programming languages - - <string> a sequence of characters wrapped with the delimiter " - every valid UTF-8 character whose code point is greater than U+001F is accepted eccept " \ - the next commonly accepted escape sequences are recognized: \0 \a \b \t \n \v \f \r \e \" \\ - morover, the escape sequences \x <two hexadecimal digits> and \u <four hexadecimal digits> - allow to specify a character by its code point - finally the escape sequences \( for U+0002 and \) for U+0003 are available - - <qualifier> the character : - - <left> each of the characters ( < [ { - this token starts a compound symbolic expression - - <right> each of the characters ) > ] } - this token ends a compound symbolic expression - - <ignored> each of the characters U+0009..U+000D U+0020 , ; = - these characters are ignored and separate the other tokens - - <reserved> any character not starting any other token - these characters are not allowed, - and those in the range U+0021..U+007E are - ! # $ % & ' * / ? @ \ ^ ` | ~ - + + + Landau's "Grundlagen der Analysis" + (from Jutting's specification in Automath). + + + + static pages (updated ), + data set (updated ), + HELM server URL (updated ). + + + + + Grundlagen's definition "t234" + in λδ version 4. +