From dfa1cda217f6b9a871ecbdd9bc54920f4a78d301 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 14 Jun 2021 16:28:21 +0200 Subject: [PATCH] =?utf8?q?=CE=BB=CE=B4=20site=20update?= MIME-Version: 1.0 Content-Type: text/plain; charset=utf8 Content-Transfer-Encoding: 8bit + one citation added to home page + one bug fixed in xhtbl.ml + ome comment added in gcp_cr.ma --- helm/www/lambdadelta/web/home/home.ldw.xml | 6 +++ .../contribs/lambdadelta/bin/xhtbl/xhtbl.ml | 41 ++++++++++--------- .../lambdadelta/static_2/static/gcp_cr.ma | 2 +- 3 files changed, 29 insertions(+), 20 deletions(-) diff --git a/helm/www/lambdadelta/web/home/home.ldw.xml b/helm/www/lambdadelta/web/home/home.ldw.xml index ec5cf0d07..d12eea80c 100644 --- a/helm/www/lambdadelta/web/home/home.ldw.xml +++ b/helm/www/lambdadelta/web/home/home.ldw.xml @@ -59,6 +59,12 @@ This is a list of publications citing λδ documentation. + + Yaoshun Fu, Wensheng Yu: + Formalizing Calculus without Limit Theory in Coq + (2021). In Mathematics, 9(12), pp. 1377:1-1377:24. + + M. Weber: An extended type system with lambda-typed lambda-expressions diff --git a/matita/matita/contribs/lambdadelta/bin/xhtbl/xhtbl.ml b/matita/matita/contribs/lambdadelta/bin/xhtbl/xhtbl.ml index 6c5f8b01f..0def8fa61 100644 --- a/matita/matita/contribs/lambdadelta/bin/xhtbl/xhtbl.ml +++ b/matita/matita/contribs/lambdadelta/bin/xhtbl/xhtbl.ml @@ -2,7 +2,7 @@ module A = Arg module F = Filename module L = List -module O = Options +module O = Options module TP = TextParser module TL = TextLexer module TU = TextUnparser @@ -48,30 +48,33 @@ let process_directive och bname (name, table, css, uri, ext) = let process_file fname = let bname = F.chop_extension (F.basename fname) in - let ich = open_in fname in - let lexbuf = Lexing.from_channel ich in - let ns, ds = TP.script TL.token lexbuf in - close_in ich; includes := bname :: !includes; - let ns = ("", "http://www.w3.org/1999/xhtml") :: ns in - let och = XU.open_out bname ns in - L.iter (process_directive och bname) ds; - XU.close_out och + if List.mem bname !includes then () + else begin + let ich = open_in fname in + let lexbuf = Lexing.from_channel ich in + let ns, ds = TP.script TL.token lexbuf in + close_in ich; includes := bname :: !includes; + let ns = ("", "http://www.w3.org/1999/xhtml") :: ns in + let och = XU.open_out bname ns in + L.iter (process_directive och bname) ds; + XU.close_out och + end let main () = A.parse [ "-L", A.Set O.debug_lexer, help_L; - "-O", A.String ((:=) O.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; - "-e1", A.Set O.e1, help_e1; - "-e2", A.Set O.e2, help_e2; - "-p0", A.Set O.p0, help_p0; - "-p1", A.Set O.p1, help_p1; - "-p2", A.Set O.p2, help_p2; + "-d0", A.Set O.d0, help_d0; + "-d1", A.Set O.d1, help_d1; + "-d2", A.Set O.d2, help_d2; + "-e1", A.Set O.e1, help_e1; + "-e2", A.Set O.e2, help_e2; + "-p0", A.Set O.p0, help_p0; + "-p1", A.Set O.p1, help_p1; + "-p2", A.Set O.p2, help_p2; ] process_file help; - XU.write_hook hook !includes !tables + XU.write_hook hook !includes !tables let _ = main () diff --git a/matita/matita/contribs/lambdadelta/static_2/static/gcp_cr.ma b/matita/matita/contribs/lambdadelta/static_2/static/gcp_cr.ma index 589fc597c..a064c7e1f 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/gcp_cr.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/gcp_cr.ma @@ -30,7 +30,7 @@ definition S2 ≝ λRR:relation4 genv lenv term term. λRS:relation term. λRP,C ∀G,L,Vs. all … (RP G L) Vs → ∀T. 𝐒❪T❫ → nf RR RS G L T → C G L (ⒶVs.T). -(* Note: this generalizes Tait's ii *) +(* Note: this generalizes Tait's ii, or Girard's CR3 *) definition S3 ≝ λC:candidate. ∀a,G,L,Vs,V,T,W. C G L (ⒶVs.ⓓ[a]ⓝW.V.T) → C G L (ⒶVs.ⓐV.ⓛ[a]W.T). -- 2.39.2