]> matita.cs.unibo.it Git - helm.git/log
helm.git
12 years agoAdded weak realizability.
Wilmer Ricciotti [Wed, 2 May 2012 10:33:18 +0000 (10:33 +0000)]
Added weak realizability.

12 years agoAdded wmono.
Andrea Asperti [Wed, 2 May 2012 09:15:19 +0000 (09:15 +0000)]
Added wmono.

12 years agoMore proofs in if-then-else machine.
Wilmer Ricciotti [Mon, 30 Apr 2012 15:12:42 +0000 (15:12 +0000)]
More proofs in if-then-else machine.

12 years agoLe configurazioni sono definite non su macchine ma su stati.
Andrea Asperti [Mon, 30 Apr 2012 10:44:36 +0000 (10:44 +0000)]
Le configurazioni sono definite non su macchine ma su stati.
Idem per alcune funzioni di lift.

12 years agoDefinition of accRealize
Andrea Asperti [Mon, 30 Apr 2012 09:29:09 +0000 (09:29 +0000)]
Definition of accRealize

12 years agoIf machine
Andrea Asperti [Mon, 30 Apr 2012 08:44:34 +0000 (08:44 +0000)]
If machine

12 years agoMonotape turing machines update.
Wilmer Ricciotti [Mon, 30 Apr 2012 07:16:17 +0000 (07:16 +0000)]
Monotape turing machines update.

12 years agomore loop proofs
Wilmer Ricciotti [Fri, 27 Apr 2012 16:42:29 +0000 (16:42 +0000)]
more loop proofs

12 years agoloop functions
Wilmer Ricciotti [Fri, 27 Apr 2012 15:20:22 +0000 (15:20 +0000)]
loop functions

12 years agoloop functions
Andrea Asperti [Fri, 27 Apr 2012 15:19:23 +0000 (15:19 +0000)]
loop functions

12 years agoMono tape turing machines
Andrea Asperti [Fri, 27 Apr 2012 11:47:09 +0000 (11:47 +0000)]
Mono tape turing machines

12 years agoExtensions to finset (sum) and auxiliary lemmas.
Andrea Asperti [Fri, 27 Apr 2012 11:46:07 +0000 (11:46 +0000)]
Extensions to finset (sum) and auxiliary lemmas.

12 years ago- notation (possibly affecting all .ma files):
Ferruccio Guidi [Thu, 26 Apr 2012 15:28:13 +0000 (15:28 +0000)]
- notation (possibly affecting all .ma files):
  we shifted the precedence levels from 50 to 60 up by 5
  and moved level 65 to 66. By so doing, we cleared level 50 for
  use in the specification of the formal system lambda_delta,
  where we use it for weakly binding constructors
- lambda_delta:
  notation fixup (a couple of bugs were corrected)

12 years agoadditions in basic_2
Ferruccio Guidi [Wed, 25 Apr 2012 16:05:54 +0000 (16:05 +0000)]
additions in basic_2

12 years ago- lambda_delta: bug fix in static type assignment
Ferruccio Guidi [Wed, 25 Apr 2012 15:54:27 +0000 (15:54 +0000)]
- lambda_delta: bug fix in static type assignment
                some theorems on delift and thin
- nat: eliminator for nat with "+1" rather than "S"

12 years agoUpdate to universal turing machine (preliminaries).
Wilmer Ricciotti [Tue, 24 Apr 2012 16:12:01 +0000 (16:12 +0000)]
Update to universal turing machine (preliminaries).

12 years agoMore turing machines (still not compiling)
Wilmer Ricciotti [Tue, 24 Apr 2012 12:35:49 +0000 (12:35 +0000)]
More turing machines (still not compiling)

12 years agoStarted converting informal definition of the machines to matita code
Wilmer Ricciotti [Tue, 24 Apr 2012 10:52:41 +0000 (10:52 +0000)]
Started converting informal definition of the machines to matita code
(currently not compiling).

12 years agoAdded universal turing machines (only comments for now).
Wilmer Ricciotti [Mon, 23 Apr 2012 11:33:11 +0000 (11:33 +0000)]
Added universal turing machines (only comments for now).

12 years agoadditions to basic_2
Ferruccio Guidi [Sat, 21 Apr 2012 13:27:53 +0000 (13:27 +0000)]
additions to basic_2

12 years ago- lambda_delta: static type assignment is defined
Ferruccio Guidi [Sat, 21 Apr 2012 13:20:21 +0000 (13:20 +0000)]
- lambda_delta: static type assignment is defined
- predefined_virtuals: some additions
- nat: we added a lemma

12 years ago- update in basic_2
Ferruccio Guidi [Thu, 19 Apr 2012 13:16:47 +0000 (13:16 +0000)]
- update in basic_2

12 years ago- firs theorems on native type assignment
Ferruccio Guidi [Thu, 19 Apr 2012 13:06:00 +0000 (13:06 +0000)]
- firs theorems on native type assignment
- we removed iterated unfold on local environments
  since transitivity of this unfold is not needed so far

12 years agoFixed w.r.t. new yelp.
Claudio Sacerdoti Coen [Tue, 17 Apr 2012 14:07:27 +0000 (14:07 +0000)]
Fixed w.r.t. new yelp.

12 years ago- milestone update in basic_2
Ferruccio Guidi [Mon, 16 Apr 2012 15:08:39 +0000 (15:08 +0000)]
- milestone update in basic_2
- html bugfix in hand written web pages

12 years ago- subject equivalence for atomic arity assignment completed!
Ferruccio Guidi [Mon, 16 Apr 2012 14:45:39 +0000 (14:45 +0000)]
- subject equivalence for atomic arity assignment completed!
- bug fix in partial unfold for local environments (nowthis relation
is confluent)

12 years agoDefinition of complexity
Andrea Asperti [Fri, 13 Apr 2012 10:24:39 +0000 (10:24 +0000)]
Definition of complexity

12 years agocommit by user ricciott
matitaweb [Tue, 10 Apr 2012 17:15:10 +0000 (17:15 +0000)]
commit by user ricciott

12 years agocommit by user
matitaweb [Tue, 10 Apr 2012 17:15:08 +0000 (17:15 +0000)]
commit by user

12 years agourgent partial commit ... to be fixed later ...
Ferruccio Guidi [Tue, 10 Apr 2012 13:50:40 +0000 (13:50 +0000)]
urgent partial commit ... to be fixed later ...

12 years agourgent partial commit ... to be fixed later ...
Ferruccio Guidi [Tue, 10 Apr 2012 13:48:26 +0000 (13:48 +0000)]
urgent partial commit ... to be fixed later ...

12 years agoupdate in basic_2
Ferruccio Guidi [Wed, 4 Apr 2012 18:52:03 +0000 (18:52 +0000)]
update in basic_2

12 years ago- some work on context equivalence of atomic arity assignment
Ferruccio Guidi [Wed, 4 Apr 2012 18:47:28 +0000 (18:47 +0000)]
- some work on context equivalence of atomic arity assignment

12 years agoAdded in basics
Andrea Asperti [Wed, 4 Apr 2012 07:28:38 +0000 (07:28 +0000)]
Added in basics
- vectors.ma
- finset.ma

Added turing

minor ntegrations in list,ma and listb.ma

12 years agoMinor changes
Andrea Asperti [Tue, 3 Apr 2012 15:36:09 +0000 (15:36 +0000)]
Minor changes

12 years agoMore changes to the website (matitaweb).
Wilmer Ricciotti [Tue, 3 Apr 2012 13:33:04 +0000 (13:33 +0000)]
More changes to the website (matitaweb).

12 years agoVarious updates to the (obsolete) website.
Wilmer Ricciotti [Tue, 3 Apr 2012 11:31:03 +0000 (11:31 +0000)]
Various updates to the (obsolete) website.

12 years agomodifiche
Andrea Asperti [Tue, 3 Apr 2012 10:37:54 +0000 (10:37 +0000)]
modifiche

12 years agoVersione italiana
Andrea Asperti [Tue, 3 Apr 2012 09:17:00 +0000 (09:17 +0000)]
Versione italiana

12 years agoNew home
Andrea Asperti [Tue, 3 Apr 2012 08:55:02 +0000 (08:55 +0000)]
New home

12 years agoTop picture
Andrea Asperti [Tue, 3 Apr 2012 08:41:08 +0000 (08:41 +0000)]
Top picture

12 years agoprova
Andrea Asperti [Tue, 3 Apr 2012 08:35:11 +0000 (08:35 +0000)]
prova

12 years agoCreated a new directory for Matita1.0
Andrea Asperti [Tue, 3 Apr 2012 07:46:45 +0000 (07:46 +0000)]
Created a new directory for Matita1.0

12 years agoadditions to basic_2
Ferruccio Guidi [Fri, 30 Mar 2012 18:20:31 +0000 (18:20 +0000)]
additions to basic_2

12 years ago- more on subject reduction of atomic arity assignment
Ferruccio Guidi [Fri, 30 Mar 2012 18:15:10 +0000 (18:15 +0000)]
- more on subject reduction of atomic arity assignment
- some results on context-sensitive equivalence of terms

12 years agomanual commit
matitaweb [Wed, 28 Mar 2012 08:22:32 +0000 (08:22 +0000)]
manual commit

12 years agoMatitaweb:
Wilmer Ricciotti [Tue, 27 Mar 2012 12:23:00 +0000 (12:23 +0000)]
Matitaweb:

Improved support for notations enriched with hyperlinks.
This revision introduces a "ref" keyword which can be used in the lefthand side
of notation statements. "ref" can only be used to decorate literals (i.e.
symbols, numbers, or keywords). The syntax is as follows:

  LITERAL ::= SIMPLE_LITERAL
           |  ref CSYMBOL SIMPLE_LITERAL

For example, the notation

  ref 'cons [ list0 x sep ; ref 'nil ]

used as the compact notation for lists specifies that the `[' symbol will be
enriched with the interpretation of 'cons nodes of the AST, and the `]' symbol
with the interpretation of 'nil nodes of the AST.

12 years agoadditions in basic_2
Ferruccio Guidi [Fri, 23 Mar 2012 14:46:23 +0000 (14:46 +0000)]
additions in basic_2

12 years ago- pts: we restored the former hierarchy
Ferruccio Guidi [Fri, 23 Mar 2012 14:40:59 +0000 (14:40 +0000)]
- pts: we restored the former hierarchy
- nat: we added a missing lemma
- lambda_delta: subject reduction continues ...

12 years agoMatitaweb: Fixes a bug in the extensible parser which caused Matita to crash
Wilmer Ricciotti [Fri, 23 Mar 2012 10:24:22 +0000 (10:24 +0000)]
Matitaweb: Fixes a bug in the extensible parser which caused Matita to crash
when parsing a notation using keywords (rather than symbols). The semantic
action associated to the notation was expecting the parser to decorate the
keyword token with its location: this was not happening, causing a runtime
type exception.

12 years agoMatitaweb: Fixes a bug which prevented Mozilla from displaying long goals
Wilmer Ricciotti [Fri, 23 Mar 2012 10:11:15 +0000 (10:11 +0000)]
Matitaweb: Fixes a bug which prevented Mozilla from displaying long goals
correctly.

12 years agocommit by user andrea
matitaweb [Fri, 23 Mar 2012 09:23:59 +0000 (09:23 +0000)]
commit by user andrea

12 years agocommit by user utente2
matitaweb [Fri, 23 Mar 2012 08:52:03 +0000 (08:52 +0000)]
commit by user utente2

12 years agocommit by user
matitaweb [Fri, 23 Mar 2012 08:51:40 +0000 (08:51 +0000)]
commit by user

12 years agocommit by user ricciott
matitaweb [Fri, 23 Mar 2012 08:51:16 +0000 (08:51 +0000)]
commit by user ricciott

12 years agocommit by user andrea
matitaweb [Fri, 23 Mar 2012 08:51:09 +0000 (08:51 +0000)]
commit by user andrea

12 years agoMatitaweb:
matitaweb [Tue, 20 Mar 2012 16:27:14 +0000 (16:27 +0000)]
Matitaweb:
1) partially solves a problem with TeX-like macro conversion when the script contains markup
2) ports a bugfix from Matita 1.0 (see log for revision 11211).

12 years agoadditions to basic_2
Ferruccio Guidi [Mon, 19 Mar 2012 15:32:58 +0000 (15:32 +0000)]
additions to basic_2

12 years ago- basics: bug fix in Conf3, it was not generic enough
Ferruccio Guidi [Mon, 19 Mar 2012 15:11:24 +0000 (15:11 +0000)]
- basics: bug fix in Conf3, it was not generic enough
- lambda_delta: subject reduction of static typestarted ...

12 years agoupdate in basic_2 and apps_2
Ferruccio Guidi [Sat, 17 Mar 2012 17:11:18 +0000 (17:11 +0000)]
update in basic_2 and apps_2

12 years ago- basics: some support for abstract triangular confluence (which
Ferruccio Guidi [Sat, 17 Mar 2012 16:51:06 +0000 (16:51 +0000)]
- basics: some support for abstract triangular confluence (which
subject reduction is an instance of)
- predefined_virtuals: more Alt-L shortcuts
- lambda_delta: more properties on computation, some annotations,
improved Makefile

12 years agorenaming completed
Ferruccio Guidi [Thu, 15 Mar 2012 19:03:49 +0000 (19:03 +0000)]
renaming completed

12 years agosome renaming (ld_ prefix removed from file names)
Ferruccio Guidi [Thu, 15 Mar 2012 18:57:05 +0000 (18:57 +0000)]
some renaming (ld_ prefix removed from file names)

12 years agosome renaming: ld_ prefix removed
Ferruccio Guidi [Thu, 15 Mar 2012 18:49:25 +0000 (18:49 +0000)]
some renaming: ld_ prefix removed

12 years agomilestone update in basic_2!
Ferruccio Guidi [Thu, 15 Mar 2012 18:27:33 +0000 (18:27 +0000)]
milestone update in basic_2!

12 years ago- lambda_delta: strong normalization of simply typed terms closed!
Ferruccio Guidi [Thu, 15 Mar 2012 18:00:48 +0000 (18:00 +0000)]
- lambda_delta: strong normalization of simply typed terms closed!
- star.ma: transitive closure: support for reverse elimination

12 years agoManual commit (basics/core_notation.ma)
matitaweb [Thu, 15 Mar 2012 10:33:00 +0000 (10:33 +0000)]
Manual commit (basics/core_notation.ma)

12 years agoupdate in basic_2
Ferruccio Guidi [Wed, 14 Mar 2012 20:04:04 +0000 (20:04 +0000)]
update in basic_2

12 years agoproperty S2 of strongly normalizing terms proved!
Ferruccio Guidi [Wed, 14 Mar 2012 19:53:16 +0000 (19:53 +0000)]
property S2 of strongly normalizing terms proved!

12 years ago- property S4 of strongly normalizing term proved!
Ferruccio Guidi [Wed, 14 Mar 2012 15:39:49 +0000 (15:39 +0000)]
- property S4 of strongly normalizing term proved!

12 years agomanual correction to tutorial/chapter2.ma
matitaweb [Tue, 13 Mar 2012 15:12:07 +0000 (15:12 +0000)]
manual correction to tutorial/chapter2.ma

12 years ago- Properties S3 and S5 of context-sensitive strongly normalizing terms
Ferruccio Guidi [Mon, 12 Mar 2012 17:05:13 +0000 (17:05 +0000)]
- Properties S3 and S5 of context-sensitive strongly normalizing terms
proved!
- more properties of context-sensitive computation

12 years ago(no commit message)
matitaweb [Mon, 12 Mar 2012 14:56:10 +0000 (14:56 +0000)]

12 years agoMatitaweb:
matitaweb [Mon, 12 Mar 2012 08:47:22 +0000 (08:47 +0000)]
Matitaweb:

1) Solves a bug in "Del hrefs"

2) Solves interaction glitches related to the disambiguation/error
reporting interface

3) Fixes the implementation of the Upload feature

4) Adds support for "low-users", who don't have permission to commit

5) Solves problems related to the multi-user mode

6) Limits direct file access to the html/ subdir of the Matita
installation (for security); all the files that must be accessed by a
web browser have been moved there

7) utf8macrotable.js uses numeric html entities instead of named
entities, to cope with incoherent behaviour of web browsers (named
entities being resolved to different unicode characters -- possible
bug in the web browser).

8) disables many debug prints

12 years ago- context-sensitive computation: more properties
Ferruccio Guidi [Sun, 11 Mar 2012 19:30:07 +0000 (19:30 +0000)]
- context-sensitive computation: more properties
- context-sensitive reduction: bug fix in a lemma's name
- some annotations added

12 years agogenerated web pages update
Ferruccio Guidi [Sat, 10 Mar 2012 19:07:03 +0000 (19:07 +0000)]
generated web pages update

12 years ago- renaming completed!
Ferruccio Guidi [Sat, 10 Mar 2012 19:03:31 +0000 (19:03 +0000)]
- renaming completed!
- one more property of context-sensitive computation
- improved Makefile (from former commit)

12 years agoWe are decapitalizing the contributions' names ...
Ferruccio Guidi [Sat, 10 Mar 2012 14:46:11 +0000 (14:46 +0000)]
We are decapitalizing the contributions' names ...

12 years ago- update in Basic_2
Ferruccio Guidi [Fri, 9 Mar 2012 17:38:40 +0000 (17:38 +0000)]
- update in Basic_2
- we added some information in thesunnary tables

12 years ago- lambda_delta: morew propertie in context-sensitive computation
Ferruccio Guidi [Fri, 9 Mar 2012 17:31:33 +0000 (17:31 +0000)]
- lambda_delta: morew propertie in context-sensitive computation
- formal_topology: compilation of categories.ma continues ...
- grafiteEngine.ml: coercions to sorts can now be defined with the short
syntax

12 years agoFixes bug where switching to a new tab the slider is not updated correctly.
Claudio Sacerdoti Coen [Fri, 9 Mar 2012 16:34:21 +0000 (16:34 +0000)]
Fixes bug where switching to a new tab the slider is not updated correctly.

12 years agocommit by user andrea
matitaweb [Thu, 8 Mar 2012 10:02:01 +0000 (10:02 +0000)]
commit by user andrea

12 years agocommit by user andrea
matitaweb [Thu, 8 Mar 2012 08:24:25 +0000 (08:24 +0000)]
commit by user andrea

12 years agocommit by user andrea
matitaweb [Thu, 8 Mar 2012 07:55:11 +0000 (07:55 +0000)]
commit by user andrea

12 years agocommit by user utente2
matitaweb [Thu, 8 Mar 2012 07:43:40 +0000 (07:43 +0000)]
commit by user utente2

12 years agocommit by user ricciott
matitaweb [Thu, 8 Mar 2012 07:43:23 +0000 (07:43 +0000)]
commit by user ricciott

12 years agocommit by user andrea
matitaweb [Thu, 8 Mar 2012 07:43:21 +0000 (07:43 +0000)]
commit by user andrea

12 years agoAxiom proved
Andrea Asperti [Thu, 8 Mar 2012 07:38:38 +0000 (07:38 +0000)]
Axiom proved

12 years agoSectionin
matitaweb [Thu, 8 Mar 2012 07:21:22 +0000 (07:21 +0000)]
Sectionin

12 years agocommit by user utente2
matitaweb [Wed, 7 Mar 2012 11:50:58 +0000 (11:50 +0000)]
commit by user utente2

12 years agocommit by user andrea
matitaweb [Wed, 7 Mar 2012 11:50:55 +0000 (11:50 +0000)]
commit by user andrea

12 years agomore sections
matitaweb [Wed, 7 Mar 2012 11:47:26 +0000 (11:47 +0000)]
more sections

12 years agosmall changes
matitaweb [Wed, 7 Mar 2012 11:41:23 +0000 (11:41 +0000)]
small changes

12 years agoTitols
matitaweb [Wed, 7 Mar 2012 11:40:06 +0000 (11:40 +0000)]
Titols

12 years agoSections
matitaweb [Wed, 7 Mar 2012 11:37:19 +0000 (11:37 +0000)]
Sections

12 years agocommit by user andrea
matitaweb [Wed, 7 Mar 2012 10:37:08 +0000 (10:37 +0000)]
commit by user andrea

12 years agocommit by user utente2
matitaweb [Wed, 7 Mar 2012 10:37:05 +0000 (10:37 +0000)]
commit by user utente2

12 years agosection in chapter 2
matitaweb [Wed, 7 Mar 2012 10:26:46 +0000 (10:26 +0000)]
section in chapter 2

12 years agocommit by user andrea
matitaweb [Wed, 7 Mar 2012 10:13:47 +0000 (10:13 +0000)]
commit by user andrea

12 years agoAdded sections in chapter 1.
matitaweb [Wed, 7 Mar 2012 10:01:30 +0000 (10:01 +0000)]
Added sections in chapter 1.