<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sat, 05 Jul 2014 12:39:48 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 06 Jul 2014 16:29:26 +0200</div>
</body>
</html>
$(XSLS): $(TBLS) $(XHTBL)
@echo " XHTBL *.tbl"
- $(H)$(XHTBL) -O $(XSLTDIR) $(TBLS)
+ $(H)$(XHTBL) -b $(LDURL) -O $(XSLTDIR) $(TBLS)
$(foreach LDW,$(LDWS),$(eval $(call HTML_TEMPLATE,$(LDW),$(notdir $(LDW:%.ldw.xml=%)))))
endif
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sat, 05 Jul 2014 12:39:48 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 06 Jul 2014 16:29:26 +0200</div>
</body>
</html>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sat, 05 Jul 2014 12:39:48 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 06 Jul 2014 16:29:26 +0200</div>
</body>
</html>
--- /dev/null
+module L = List
+
+module T = Table
+
+(* true for a row specification *)
+type 'a atom = 'a * bool * int option * int option
+
+type 'a atoms = 'a atom list
+
+let get_attr concat null a y x =
+ let map y x (c, b, x1, x2) = match b, x1, x2 with
+ | _ , None, None -> c
+ | false, None, Some c2 -> if x <= c2 then c else null
+ | false, Some c1, None -> if x >= c1 then c else null
+ | false, Some c1, Some c2 -> if x >= c1 && x <= c2 then c else null
+ | true , None, Some r2 -> if y <= r2 then c else null
+ | true , Some r1, None -> if y >= r1 then c else null
+ | true , Some r1, Some r2 -> if y >= r1 && y <= r2 then c else null
+ in
+ concat (L.map (map y x) a)
+++ /dev/null
-module L = List
-
-module T = Table
-
-(* true for a row specification *)
-type atom = T.css * bool * int option * int option
-
-type atoms = atom list
-
-let get_css a y x =
- let map y x (c, b, x1, x2) = match b, x1, x2 with
- | _ , None, None -> c
- | false, None, Some c2 -> if x <= c2 then c else []
- | false, Some c1, None -> if x >= c1 then c else []
- | false, Some c1, Some c2 -> if x >= c1 && x <= c2 then c else []
- | true , None, Some r2 -> if y <= r2 then c else []
- | true , Some r1, None -> if y >= r1 then c else []
- | true , Some r1, Some r2 -> if y >= r1 && y <= r2 then c else []
- in
- L.concat (L.map (map y x) a)
module A = Array
+module N = Filename
module T = Table
type cell = {
ck: T.text list; (* contents *)
cc: T.css; (* css classes *)
+ cu: T.uri; (* uri *)
+ cx: T.ext; (* extension *)
cb: T.border; (* border *)
}
}
let empty = {
- ck = []; cc = []; cb = T.border false;
+ ck = []; cc = []; cu = ""; cx = ""; cb = T.border false;
}
let make ts = {
let set_key m y x kl =
m.m.(y).(x) <- {m.m.(y).(x) with ck = kl}
-let set_css m y x c =
- m.m.(y).(x) <- {m.m.(y).(x) with cc = c @ m.m.(y).(x).cc}
+let set_attrs m y x c u e =
+ m.m.(y).(x) <- {m.m.(y).(x) with
+ cc = c @ m.m.(y).(x).cc;
+ cu = u ^ m.m.(y).(x).cu;
+ cx = m.m.(y).(x).cx ^ e;
+ }
let set_west m y x b =
let c = m.m.(y).(x) in
let output_dir_default = ""
+let baseuri_default = ""
+
let debug_lexer_default = false
let debug_pass_default = false
let output_dir = ref output_dir_default
+let baseuri = ref baseuri_default
+
let debug_lexer = ref debug_lexer_default
let d0 = ref debug_pass_default
let clear () =
output_dir := output_dir_default;
+ baseuri := baseuri_default;
debug_lexer := debug_lexer_default;
d0 := debug_pass_default; d1 := debug_pass_default; d2 := debug_pass_default;
e1 := debug_pass_default; e2 := debug_pass_default;
type status = {
ts: T.size; (* current dimensions *)
tc: T.css; (* current class *)
+ tu: T.uri; (* current uri *)
+ tx: T.ext; (* current extension *)
}
let empty = {
- ts = T.no_size; tc = [];
+ ts = T.no_size; tc = []; tu = ""; tx = ""
}
let init b ts =
(****************************************************************************)
let open_table st t =
- t.T.tc <- t.T.tc @ st.tc;
- {st with tc = t.T.tc}
+ t.T.tc <- t.T.tc @ st.tc; t.T.tu <- st.tu ^ t.T.tu; t.T.tx <- st.tx ^ t.T.tx;
+ {st with tc = t.T.tc; tu = t.T.tu; tx = t.T.tx}
let close_table st t =
t.T.ts <- st.ts; st
| T.Key (T.Text sl) -> M.set_key st.tm t.T.ts.T.y t.T.ts.T.x sl
| _ -> ()
-let set_css st t =
+let set_attrs st t =
let rec aux y x =
if y >= t.T.ts.T.rf then () else
if x >= t.T.ts.T.cf then aux (succ y) 0 else begin
- M.set_css st.tm (t.T.ts.T.y + y) (t.T.ts.T.x + x) t.T.tc;
+ M.set_attrs st.tm (t.T.ts.T.y + y) (t.T.ts.T.x + x) t.T.tc t.T.tu t.T.tx;
aux y (succ x)
end
in
print st t; st
let close_table st t =
- set_key st t; set_css st t; set_borders st t; st
+ set_key st t; set_attrs st t; set_borders st t; st
let map_key st k = st
-module A = Array
+module L = List
+module S = String
+module V = Array
+module T = Table
module M = Matrix
-module C = Css
+module A = Attr
type status = {
m: M.matrix;
- a: C.atoms;
+ c: T.css A.atoms;
+ u: T.uri A.atoms;
+ x: T.ext A.atoms;
}
-let initial a m = {
- m = m; a = a;
+let initial c u x m = {
+ m = m; c = c; u = u; x = x
}
let process_cell st y x c =
- M.set_css st.m y x (C.get_css st.a y x)
+ M.set_attrs st.m y x
+ (A.get_attr L.concat [] st.c y x)
+ (A.get_attr (S.concat "") "" st.u y x)
+ (A.get_attr (S.concat "") "" st.x y x)
let process_row st y row =
- A.iteri (process_cell st y) row
+ V.iteri (process_cell st y) row
-let process css matrix =
- let st = initial css matrix in
- A.iteri (process_row st) matrix.M.m
+let process css uri ext matrix =
+ let st = initial css uri ext matrix in
+ V.iteri (process_row st) matrix.M.m
type css = string list
+type uri = string
+
+type ext = string
+
+type absolute = bool
+
type size = {
y : int; (* first row *)
x : int; (* first column *)
}
type text = Plain of string
- | Link of string * string
+ | Link of absolute * string * string
type key = Text of text list
| Glue of int option
type table = {
mutable tc: css; (* css classes *)
+ mutable tu: uri; (* uri *)
+ mutable tx: ext; (* uri extension *)
mutable ts: size; (* dimension *)
tb: border; (* border *)
te: entry; (* contents *)
n = b; s = b; e = b; w = b;
}
-let mk_key k tc = {
- ts = no_size; tb = border false; te = Key k; tc = tc;
+let mk_key k tc tu tx = {
+ ts = no_size; tb = border false; te = Key k;
+ tc = tc; tu = tu; tx = tx;
ti = id ();
}
-let mk_line b tl tc = {
- ts = no_size; tb = border b; te = Line (b, tl); tc = tc;
+let mk_line b tl tc tu tx = {
+ ts = no_size; tb = border b; te = Line (b, tl);
+ tc = tc; tu = tu; tx = tx;
ti = id ();
}
| "(" { out "("; TP.OP }
| ")" { out ")"; TP.CP }
| "@" { out ")"; TP.AT }
- | "space" { out "name"; TP.SPACE }
+ | "space" { out "space"; TP.SPACE }
| "name" { out "name"; TP.NAME }
| "table" { out "table"; TP.TABLE }
| "class" { out "class"; TP.CSS }
+ | "uri" { out "uri"; TP.URI }
+ | "ext" { out "ext"; TP.EXT }
| eof { TP.EOF }
and str = parse
| QT { "" }
+ | "\\\\" { "\\" ^ str lexbuf }
| "\\\"" { "\"" ^ str lexbuf }
| _ as c { S.make 1 c ^ str lexbuf }
and block = parse
let split s =
S.split (S.regexp "[ \r\n\t]+") s
-let mk_atom s rs =
- let map c (b, (x1, x2)) = c, b, x1, x2 in
- L.map (map (split s)) rs
+let mk_css_atom s rs =
+ let cs = split s in
+ let map (b, (x1, x2)) = cs, b, x1, x2 in
+ L.map map rs
+
+let mk_string_atom s rs =
+ let map (b, (x1, x2)) = s, b, x1, x2 in
+ L.map map rs
%}
%token <int> NUM
%token <string> TEXT
-%token SPACE NAME TABLE CSS SR OC CC OB CB PS OP CP AT EOF
+%token SPACE NAME TABLE CSS URI EXT SR OC CC OB CB PS OP CP AT EOF
%start script
-%type <(string * string) list * (string * Table.table * Css.atoms) list> script
+%type <(string * string) list * (string * Table.table * Table.css Attr.atoms * Table.uri Attr.atoms * Table.ext Attr.atoms) list> script
%%
;
text:
- | TEXT { T.Plain $1 }
- | AT OP TEXT TEXT CP { T.Link ($3, $4) }
+ | TEXT { T.Plain $1 }
+ | AT OP TEXT TEXT CP { T.Link (true, $3, $4) }
+ | AT AT OP TEXT TEXT CP { T.Link (false, $4, $5) }
+ | AT TEXT { T.Link (true, $2, $2) }
+ | AT AT TEXT { T.Link (false, $3, $3) }
;
texts:
| CSS TEXT { split $2 }
;
+uri:
+ | { "" }
+ | URI TEXT { $2 }
+;
+
+ext:
+ | { "" }
+ | EXT TEXT { $2 }
+;
+
table:
- | css key { T.mk_key $2 $1 }
- | css OC tables CC { T.mk_line false $3 $1 }
- | css OB tables CB { T.mk_line true $3 $1 }
+ | css uri ext key { T.mk_key $4 $1 $2 $3 }
+ | css uri ext OC tables CC { T.mk_line false $5 $1 $2 $3 }
+ | css uri ext OB tables CB { T.mk_line true $5 $1 $2 $3 }
;
tables:
| range ranges { $1 :: $2 }
;
-atom:
- | CSS TEXT ranges { mk_atom $2 $3 }
+catom:
+ | CSS TEXT ranges { mk_css_atom $2 $3 }
+;
+
+catoms:
+ | { [] }
+ | catom catoms { $1 @ $2 }
+;
+
+uatom:
+ | URI TEXT ranges { mk_string_atom $2 $3 }
+;
+
+uatoms:
+ | { [] }
+ | uatom uatoms { $1 @ $2 }
+;
+
+xatom:
+ | EXT TEXT ranges { mk_string_atom $2 $3 }
;
-atoms:
- | { [] }
- | atom atoms { $1 @ $2 }
+xatoms:
+ | { [] }
+ | xatom xatoms { $1 @ $2 }
;
directive:
- | name TABLE table atoms { $1, $3, $4 }
+ | name TABLE table catoms uatoms xatoms { $1, $3, $4, $5, $6 }
;
directives:
let css tc =
P.sprintf "\"%s\"" (S.concat " " tc)
+let uri tu tx =
+ P.sprintf "@\"%s\" \"%s\"" tu tx
+
let text = function
- | T.Plain s -> P.sprintf "\"%s\"" s
- | T.Link (uri, s) -> P.sprintf "@(\"%s\" \"%s\")" uri s
+ | T.Plain s -> P.sprintf "\"%s\"" s
+ | T.Link (true, uri, s) -> P.sprintf "@(\"%s\" \"%s\")" uri s
+ | T.Link (false, uri, s) -> P.sprintf "@@(\"%s\" \"%s\")" uri s
let key = function
| T.Text sl -> S.concat " + " (L.map text sl)
let open_table st t =
let str =
- P.sprintf "%s[{#%u: %s; %s; %s}\n"
- (indent st) t.T.ti (size t.T.ts) (border t.T.tb) (css t.T.tc)
+ P.sprintf "%s[{#%u: %s; %s; %s; %s}\n"
+ (indent st) t.T.ti (size t.T.ts) (border t.T.tb) (css t.T.tc) (uri t.T.tu t.T.tx)
in
st.out str; add st
let help_L = " Output lexer tokens"
let help_O = "<dir> Set this output directory"
let help_X = " Clear all options"
+let help_b = "<uri> Set this base uri for relative links"
let help_d0 = " Output table contents after phase zero (parsing)"
let help_d1 = " Output table contents after phase one (sizing)"
let help_d2 = " Output table contents after phase two (filling)"
let includes, tables = ref [], ref []
-let set_output_dir s = O.output_dir := s
-
-let process_directive och bname (name, table, css) =
+let process_directive och bname (name, table, css, uri, ext) =
tables := name :: !tables;
if !O.d0 then TU.debug table;
if not !O.p0 then begin
let matrix = M.make size in
let _ = P2.process table matrix in
if !O.d2 then TU.debug table;
- if not !O.p2 then P3.process css matrix;
+ if not !O.p2 then P3.process css uri ext matrix;
let name = if name = "" then bname else name in
XU.output och name matrix
end
let main () =
A.parse [
"-L", A.Set O.debug_lexer, help_L;
- "-O", A.String set_output_dir, help_O;
+ "-O", A.String ((:=) O.output_dir), help_O;
"-X", A.Unit O.clear, help_X;
+ "-b", A.String ((:=) O.baseuri), help_b;
"-d0", A.Set O.d0, help_d0;
"-d1", A.Set O.d1, help_d1;
"-d2", A.Set O.d2, help_d2;
if cell.M.cb.T.w then str.[3] <- 's';
str :: cell.M.cc
-let text = function
- | T.Plain s -> s
- | T.Link (uri, s) -> P.sprintf "<a href=\"%s\">%s</a>" uri s
+let text baseuri ext = function
+ | T.Plain s -> s
+ | T.Link (true, uri, s) -> P.sprintf "<a href=\"%s\">%s</a>" uri s
+ | T.Link (false, uri, s) ->
+ let uri = !O.baseuri ^ baseuri ^ uri ^ ext in
+ P.sprintf "<a href=\"%s\">%s</a>" uri s
let key cell =
- if cell.M.ck = [] then "<br/>" else S.concat " " (L.map text cell.M.ck)
+ if cell.M.ck = [] then "<br/>" else S.concat " " (L.map (text cell.M.cu cell.M.cx) cell.M.ck)
let ind i = S.make (2 * i) ' '
margin: 2.5%;
}
-a:link, a:visited {
+a:link, a:visited, a:hover, a:active, a:focus {
text-decoration: underline;
color: rgb(0, 0, 0);
}
-a:active, a:hover, a:focus {
+a:hover {
background: rgb(192, 192, 192);
- color: rgb(0, 0, 0);
+}
+
+/* on newer browsers, disable style modifications for named anchors */
+a[name]:hover {
+ text-decoration: inherit;
+ color: inherit;
+ background: inherit;
}
/* blocks *******************************************************************/
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sat, 05 Jul 2014 12:39:48 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 06 Jul 2014 16:29:26 +0200</div>
</body>
</html>
-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
-<html dir="ltr" lang="en-us"><head>
-
-
-
- <meta content="text/html; charset=UTF-8" http-equiv="content-type"><title>λδ home page</title>
-
- <meta content="Ferruccio Guidi" name="author">
- <meta content="The formal system λδ" name="description">
- <link rel="shortcut icon" href="images/crux_16.ico"></head><body>
-<div style="text-align: center;">
-<br>
-<a href="http://lambdadelta.info/"><img alt="[Crux Logo]" title="The Crux" src="images/crux_32.png" style="border: 0px solid ; width: 32px; height: 32px;"></a>
-<h1>The Formal System λδ (\lambda\delta)<br>
-</h1>
-<h2>Towards the unification of terms, types, environments and contexts</h2>
-<img style="width: 95%; height: 4px;" alt="[Separator]" title="Separator" src="images/rainbow.png"><br>
-<table style="text-align: left; width: 95%; margin-left: auto; margin-right: auto;" border="0" cellpadding="2" cellspacing="20">
- <tbody>
- <tr>
- <td style="vertical-align: top;">
- <ul>
- <li>Foreword</li>
- </ul>
- <ul>
- <li><a href="news.html">News</a></li>
- </ul>
- <ul>
- <li><a href="documentation.html">Papers</a></li>
- </ul>
- <ul>
- <li><a href="implementation.html">Resources</a><br>
- </li>
- </ul>
- </td>
- <td style="vertical-align: top; text-align: left;">
- <h3 style="text-align: right;">Foreword <img style="width: 37px; height: 37px;" alt="[Butterfly]" title="Butterfly" src="images/b9.png"></h3>
-The formal system λδ
-(\lambda\delta) is a typed lambda calculus that pursues the static and
-dynamic unification of terms, types, environments and contexts while
-enjoying a well-conceived theory, which includes the commonly
-desired properties.<br>
- <br>
-λδ takes some features from the calculi of the Automath family and
-some from the pure type systems, but it differs from both in that it
-does not include the Π construction while it provides for an
-abbreviation mechanism at the level of terms.<br>
- <br>
-λδ features explicit type annotations, which are borrowed from
-realistic type checker implementations and with which type checking is
-reduced to type inference.<br>
- <br>
-The reduction steps of λδ include β-contraction, δ-expansion,
-ζ-contraction and θ-swap. On the other hand,
-η-contraction is not included.<br>
- <br>
-The theory of λδ includes important properties such as the
-confluence of reduction, the correctness of types, the
-uniqueness of types up to conversion, the subject reduction of the type
-assignment, the strong normalization of the typed terms. The
-decidability of type inference and of type checking come as corollaries.<br>
- <br>
-λδ features uniformly dependent types and a predicative abstraction
-mechanism, so the calculus can serve as a formal specification language
-for the type theories that need a predicative foundation. λδ is
-expected to have the expressive power of λ→.<br>
- <br>
-λδ comes in several versions listed in the following table, which
-includes the major milestones:<br>
- <br>
- <table style="text-align: left; width: 100%;" border="1" cellpadding="2" cellspacing="0">
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1//EN" "http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml" dir="ltr" lang="en-us">
+ <head>
+ <meta http-equiv="Content-Language" content="en-us" />
+ <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
+ <meta http-equiv="Content-Style-Type" content="text/css" />
+ <meta name="author" content="Ferruccio Guidi" />
+ <meta name="description" content="\lambda\delta home page" />
+ <title>\lambda\delta home page</title>
+ <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/ld_web.css" />
+ <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/lddl.css" />
+ <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/xhtbl.css" />
+ <link rel="shortcut icon" href="http://lambdadelta.info/images/crux_16.ico" />
+ </head>
+ <body lang="en-US">
+ <div class="spacer">
+ <a href="http://lambdadelta.info/">
+ <img class="icon32" alt="[lambdadelta home]" title="lambdadelta home" src="http://lambdadelta.info/images/crux_32.png" />
+ </a>
+ </div>
+ <div class="head1">The Formal System λδ (\lambda\delta)</div>
+ <div class="spacer">
+ <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
+ </div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">
+ <br />
+ </div>
+ <div xmlns:ld="http://lambdadelta.info/" class="text">
+ <table cellpadding="4" cellspacing="0">
<tbody>
<tr>
- <td style="vertical-align: top; background-color: rgb(223, 223, 223); text-align: center;">Version<br>
+ <td class="snss component sky">
+ <a href="http://lambdadelta.info/index.html">foreword</a>
</td>
- <td style="vertical-align: top; background-color: rgb(223, 223, 223); text-align: center;">Name<br>
+ <td class="snss component magenta">
+ <a href="http://lambdadelta.info/news.html">news</a>
</td>
- <td style="vertical-align: top; background-color: rgb(223, 223, 223); text-align: center;">Started<br>
+ <td class="snss component orange">
+ <a href="http://lambdadelta.info/documentation.html">documentation</a>
</td>
- <td style="vertical-align: top; background-color: rgb(223, 223, 223); text-align: center;">Released<br>
- </td>
- <td style="vertical-align: top; background-color: rgb(223, 223, 223); text-align: center;">Dismissed<br>
+ <td class="ssss component green">
+ <a href="http://lambdadelta.info/implementation.html">implementation</a>
</td>
</tr>
+ </tbody>
+ </table>
+ </div>
+
+ <a xmlns:ld="http://lambdadelta.info/" name="foreword" />
+ <div xmlns:ld="http://lambdadelta.info/" class="head2dx">Foreword <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b9.png" />
+ </div>
+ <div xmlns:ld="http://lambdadelta.info/" class="text">
+ The formal system λδ (\lambda\delta) is a typed λ-calculus aiming to support
+ the foundations of Mathematics that require an underlying specification language
+ (for example the <a href="http://www.math.unipd.it/~maietti/">Minimal Type Theory</a>
+ and its predecessors).
+ </div>
+ <div xmlns:ld="http://lambdadelta.info/" class="text">
+ λδ is developed in the context of the
+ <a href="http://helm.cs.unibo.it/">Hypertextual Electronic Library of Mathematics</a>
+ as a machine-checked digital specification
+ that is not the formal counterpart of some previously published informal material.
+ </div>
+ <div xmlns:ld="http://lambdadelta.info/" class="text">
+ λδ comes in several versions listed in the following table,
+ which includes the major milestones:
+ </div>
+ <div xmlns:ld="http://lambdadelta.info/" class="text">
+ <table cellpadding="4" cellspacing="0">
+ <tbody>
<tr>
- <td style="vertical-align: top; background-color: rgb(255, 223, 191);">2<br>
- </td>
- <td style="vertical-align: top; background-color: rgb(255, 223, 191);">basic_2<br>
- </td>
- <td style="vertical-align: top; background-color: rgb(255, 223, 191);">April
-2011<br>
- </td>
- <td style="vertical-align: top; background-color: rgb(255, 223, 191);">planned
-in
-2014<br>
- </td>
- <td style="vertical-align: top; background-color: rgb(255, 223, 191);">not
-planned yet<br>
- </td>
+ <td class="snns component gray">version</td>
+ <td class="snnn component gray">name</td>
+ <td class="snnn component gray">developed with</td>
+ <td class="snnn component gray">started</td>
+ <td class="snnn component gray">announced</td>
+ <td class="snnn component gray">released</td>
+ <td class="ssnn component gray">dismissed</td>
</tr>
<tr>
- <td style="vertical-align: top; background-color: rgb(255, 191, 191);">1<br>
- </td>
- <td style="vertical-align: top; background-color: rgb(255, 191, 191);">basic_1<br>
- </td>
- <td style="vertical-align: top; background-color: rgb(255, 191, 191);">May
-2004<br>
+ <td class="snns orange">2</td>
+ <td class="snnn orange">basic_2</td>
+ <td class="snnn orange">
+ <a href="http://matita.cs.unibo.it/">Matita 0.99.2</a>
</td>
- <td style="vertical-align: top; background-color: rgb(255, 191, 191);">November
-2006<br>
- </td>
- <td style="vertical-align: top; background-color: rgb(255, 191, 191);">May
-2008<br>
+ <td class="snnn orange">April 2011</td>
+ <td class="snnn orange">July 2014</td>
+ <td class="snnn orange">Planned in 2014</td>
+ <td class="ssnn orange">Not planned yet</td>
+ </tr>
+ <tr>
+ <td class="snss red">1</td>
+ <td class="snsn red">basic_1</td>
+ <td class="snsn red">
+ <a href="http://coq.inria.fr/">Coq 7.3.1</a>
</td>
+ <td class="snsn red">May 2004</td>
+ <td class="snsn red">January 2006</td>
+ <td class="snsn red">November 2006</td>
+ <td class="sssn red">May 2008</td>
</tr>
</tbody>
</table>
- <br>
- <h3 style="text-align: right;">Notice
-for
-the
-Internet
-Explorer
-user <img style="width: 37px; height: 37px;" alt="[Butterfly]" title="Butterfly" src="images/b3.png"></h3>
-To view this site
-correctly, please select a font with <a href="http://www.unicode.org/">Unicode</a>
-support.
-For example <span style="font-weight: bold;">Lucida Sans Unicode</span>
-(it should be already installed on your system).
-To change the current font follow: <span style="font-weight: bold;">"Tools"
-menu
-→ "Internet
-Options" entry → "General" tab → "Fonts" button.</span><br>
- </td>
- </tr>
- </tbody>
-</table>
-<br>
-<a href="http://validator.w3.org/check?uri=referer"><img alt="[Valid HTML 4.01 Transitional]" title="Valid HTML 4.01 Transitional" src="http://www.w3.org/Icons/valid-html401" style="border: 0px solid ; width: 88px; height: 31px;"></a> <a href="http://www.anybrowser.org/campaign/"><img alt="[Use Any Browser Here]" title="Use Any Browser Here" src="images/globe_trans.png" style="border: 0px solid ; width: 147px; height: 42px;"></a> <img style="width: 88px; height: 31px;" alt="[PNG Used Here]" title="PNG Used Here" src="images/PNGnow2.png"><br>
-<br>
-Last update 2014-02-24 by <a href="http://www.cs.unibo.it/%7Efguidi/">Ferruccio
-Guidi</a><br>
-</div>
+ </div>
+
+ <a xmlns:ld="http://lambdadelta.info/" name="notice" />
+ <div xmlns:ld="http://lambdadelta.info/" class="head2dx">Notice for the Internet Explorer user <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b3.png" />
+ </div>
+ <div xmlns:ld="http://lambdadelta.info/" class="text">
+ To view this site correctly, please select a font
+ with <a href="http://www.unicode.org/">Unicode</a> support.
+ For example "Lucida Sans Unicode" (it should be already installed on your system).
+ To change the current font follow:
+ "Tools" menu → "Internet Options" entry → "General" tab → "Fonts" button.
+ </div>
-</body></html>
+ <div class="spacer">
+ <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
+ </div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">
+ <br />
+ </div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">
+ <a href="http://validator.w3.org/check?uri=referer">
+ <img class="w3c" alt="[Valid XHTML 1.1]" title="Valid XHTML 1.1" src="http://www.w3.org/Icons/valid-xhtml11-blue" />
+ </a>
+ <a href="http://jigsaw.w3.org/css-validator/check/referer">
+ <img class="w3c" alt="[Valid CSS level 2]" title="Valid CSS level 2" src="http://www.w3.org/Icons/valid-css2-blue" />
+ </a>
+ <a href="http://www.w3.org/XML/">
+ <img class="w3c" alt="[Generated from XML via XSL]" title="Generated from XML via XSL" src="http://lambdadelta.info/images/xml_xsl2.png" />
+ </a>
+ <a href="http://www.w3.org/Graphics/PNG/">
+ <img class="w3c" alt="[PNG used here]" title="PNG used here" src="http://lambdadelta.info/images/PNGnow2.png" />
+ </a>
+ <a href="http://www.anybrowser.org/campaign/">
+ <img class="w3c" alt="[Viewable with any browser]" title="Viewable with any browser" src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png" />
+ </a>
+ </div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">
+ <br />
+ </div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 06 Jul 2014 16:37:09 +0200</div>
+</body>
+</html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8"?>
+
+<page xmlns="http://lambdadelta.info/"
+ description = "\lambda\delta home page"
+ title = "\lambda\delta home page"
+ head = "The Formal System λδ (\lambda\delta)"
+>
+ <sitemap name="sitemap"/>
+
+ <section9 name="foreword">Foreword</section9>
+ <body>
+ The formal system λδ (\lambda\delta) is a typed λ-calculus aiming to support
+ the foundations of Mathematics that require an underlying specification language
+ (for example the <link to="http://www.math.unipd.it/~maietti/">Minimal Type Theory</link>
+ and its predecessors).
+ </body>
+ <body>
+ λδ is developed in the context of the
+ <link to="http://helm.cs.unibo.it/">Hypertextual Electronic Library of Mathematics</link>
+ as a machine-checked digital specification
+ that is not the formal counterpart of some previously published informal material.
+ </body>
+ <body>
+ λδ comes in several versions listed in the following table,
+ which includes the major milestones:
+ </body>
+ <table name="versions"/>
+
+ <section3 name="notice">Notice for the Internet Explorer user</section3>
+ <body>
+ To view this site correctly, please select a font
+ with <link to="http://www.unicode.org/">Unicode</link> support.
+ For example "Lucida Sans Unicode" (it should be already installed on your system).
+ To change the current font follow:
+ "Tools" menu → "Internet Options" entry → "General" tab → "Fonts" button.
+ </body>
+
+ <footer/>
+</page>
+++ /dev/null
-<?xml version="1.0" encoding="UTF-8"?>
-
-<page xmlns="http://lambdadelta.info/"
- description = "\lambda\delta home page"
- title = "\lambda\delta home page"
- head = "The Formal System λδ (\lambda\delta)"
->
- <sitemap name="sitemap"/>
-
- <section9 name="foreword">Foreword</section9>
- <body>
- The formal system λδ (\lambda\delta) is a typed λ-calculus aiming to support
- the foundations of Mathematics that require an underlying specification language
- (for example the <link to="http://www.math.unipd.it/~maietti/">Minimal Type Theory</link>
- and its predecessors).
- </body>
- <body>
- λδ is developed in the context of the
- <link to="http://helm.cs.unibo.it/">Hypertextual Electronic Library of Mathematics</link>
- as a machine-checked digital specification
- that is not the formal counterpart of some previously published informal material.
- </body>
- <body>
- λδ comes in several versions listed in the following table,
- which includes the major milestones:
- </body>
- <table name="versions"/>
-
- <section3 name="notice">Notice for the Internet Explorer user</section3>
- <body>
- To view this site correctly, please select a font
- with <link to="http://www.unicode.org/">Unicode</link> support.
- For example "Lucida Sans Unicode" (it should be already installed on your system).
- To change the current font follow:
- "Tools" menu → "Internet Options" entry → "General" tab → "Fonts" button.
- </body>
-
- <footer/>
-</page>
table [
class "sky" {
- [ "foreword" * ]
+ [ @@("index" "foreword") * ]
}
class "magenta" {
- [ "news" * ]
+ [ @@"news" * ]
}
class "orange" {
- [ "bibliography" * ]
+ [ @@"documentation" * ]
}
class "green" {
- [ "resources" * ]
+ [ @@"implementation" * ]
}
]
class "component" [ 0 ]
+
+ext ".html" [ 0 ]
projects / helm.git / commitdiff