From: Enrico Tassi Date: Wed, 14 Oct 2009 13:08:11 +0000 (+0000) Subject: ... X-Git-Tag: make_still_working~3305 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=203070c2ba3cb88305093ed8f44b34a3f23904e4;p=helm.git ... --- diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma index e98696589..2d7692648 100644 --- a/helm/software/matita/nlibrary/topology/igft.ma +++ b/helm/software/matita/nlibrary/topology/igft.ma @@ -11,6 +11,7 @@ the formalization of the paper > inductive generation of formal topologies by Stefano Berardi and Silvio Valentini. + The tutorial is by Enrico Tassi. The tutorial spends a considerable amount of effort in defining @@ -21,6 +22,12 @@ consistent allows to follow the paper in a pedantic way, and hopefully to make the formalization (at least the definitions and proved statements) readable to the author of the paper. +The formalization uses the ng (new generation) version of Matita +(that will be named 1.x when finally released). +Last stable release of the "old" system is named 0.5.7; the ng system +is cohexisting with the old one in every development release with a +version strictly grater then 0.5.7. + Orienteering ------------ @@ -72,6 +79,11 @@ implements two unusual input facilities: example W has Ω, 𝕎 and 𝐖, L has Λ, 𝕃, and 𝐋, F has Φ, … Variants are listed in the aforementioned TeX/UTF-8 table. +The syntax of terms (and types) is the one of the λ-calculus CIC +on which Matita is based. The main syntactical difference w.r.t. +the usual mathematical notation is the function application, written +`(f x y)` in place of `f(x,y)`. + Pressing `F1` opens the Matita manual. CIC (as [implemented in Matita][3]) in a nutshell