]> matita.cs.unibo.it Git - helm.git/log
helm.git
12 years agowe added the standard notation for True and False (logical constants)
Ferruccio Guidi [Tue, 15 May 2012 16:11:07 +0000 (16:11 +0000)]
we added the standard notation for True and False (logical constants)

12 years agoDivergence during indexing fixed: (? t = t') was not recognized as too flexible.
Claudio Sacerdoti Coen [Tue, 15 May 2012 13:14:17 +0000 (13:14 +0000)]
Divergence during indexing fixed: (? t = t') was not recognized as too flexible.

12 years agoSys.Break no longer caught during indexing
Claudio Sacerdoti Coen [Tue, 15 May 2012 13:12:43 +0000 (13:12 +0000)]
Sys.Break no longer caught during indexing

12 years agosempre li
Andrea Asperti [Tue, 15 May 2012 13:12:43 +0000 (13:12 +0000)]
sempre li

12 years agoAdded universal machine (mockup)
Wilmer Ricciotti [Tue, 15 May 2012 09:56:18 +0000 (09:56 +0000)]
Added universal machine (mockup)

12 years agoAdded copy machine (mockup)
Wilmer Ricciotti [Mon, 14 May 2012 16:41:07 +0000 (16:41 +0000)]
Added copy machine (mockup)

12 years agoprogresprogresss
Andrea Asperti [Mon, 14 May 2012 16:37:56 +0000 (16:37 +0000)]
progresprogresss
-

12 years agoalmost there
Andrea Asperti [Mon, 14 May 2012 15:26:56 +0000 (15:26 +0000)]
almost there

12 years agoprogress
Andrea Asperti [Mon, 14 May 2012 11:55:54 +0000 (11:55 +0000)]
progress

12 years agoDefinition of the structure of the transition table of a
Wilmer Ricciotti [Fri, 11 May 2012 17:03:27 +0000 (17:03 +0000)]
Definition of the structure of the transition table of a
simulated Turing Machine.

12 years agopoca roba
Andrea Asperti [Fri, 11 May 2012 11:59:16 +0000 (11:59 +0000)]
poca roba

12 years agorestructuring
Andrea Asperti [Fri, 11 May 2012 11:23:40 +0000 (11:23 +0000)]
restructuring

12 years agoFinished wsem_compare proof.
Wilmer Ricciotti [Fri, 11 May 2012 10:29:56 +0000 (10:29 +0000)]
Finished wsem_compare proof.

12 years agoprogress
Andrea Asperti [Fri, 11 May 2012 09:02:25 +0000 (09:02 +0000)]
progress

12 years agoProgress.
Wilmer Ricciotti [Thu, 10 May 2012 16:55:35 +0000 (16:55 +0000)]
Progress.

12 years ago- notation changes in basic_2
Ferruccio Guidi [Thu, 10 May 2012 16:02:55 +0000 (16:02 +0000)]
- notation changes in basic_2

12 years ago- predefined_virtuals: an addition
Ferruccio Guidi [Thu, 10 May 2012 15:57:36 +0000 (15:57 +0000)]
- predefined_virtuals: an addition
- lambda_delta: some notation changes

12 years agoProgress.
Wilmer Ricciotti [Thu, 10 May 2012 15:49:45 +0000 (15:49 +0000)]
Progress.

12 years agoPatch to improve the pretty-printing of error messages.
Claudio Sacerdoti Coen [Thu, 10 May 2012 14:18:17 +0000 (14:18 +0000)]
Patch to improve the pretty-printing of error messages.
Moreover, when a delift creates an ill-typed term, a more
informative error message is printed (even if later
backtracking makes it irrelevant).

12 years agoadditions to basic_2
Ferruccio Guidi [Thu, 10 May 2012 11:06:02 +0000 (11:06 +0000)]
additions to basic_2

12 years ago- lib: some additions
Ferruccio Guidi [Thu, 10 May 2012 10:58:45 +0000 (10:58 +0000)]
- lib: some additions
- lambda_delta: more properties on native type assignment
                change of notation for consand append

12 years agoSys.Break no longer captured in two places.
Claudio Sacerdoti Coen [Thu, 10 May 2012 08:11:13 +0000 (08:11 +0000)]
Sys.Break no longer captured in two places.

12 years agoaxiomatization of acc_if
Andrea Asperti [Thu, 10 May 2012 07:38:44 +0000 (07:38 +0000)]
axiomatization of acc_if

12 years agoProgress.
Wilmer Ricciotti [Wed, 9 May 2012 16:49:50 +0000 (16:49 +0000)]
Progress.

12 years agoProgress in compare.ma (some machines have been moved to tests.ma and marks.ma)
Wilmer Ricciotti [Wed, 9 May 2012 15:32:25 +0000 (15:32 +0000)]
Progress in compare.ma (some machines have been moved to tests.ma and marks.ma)

12 years agoprogress in turing/universal/compare.ma
Wilmer Ricciotti [Tue, 8 May 2012 16:09:32 +0000 (16:09 +0000)]
progress in turing/universal/compare.ma

12 years agoAdded compare auxiliary machine for universal turing machine.
Wilmer Ricciotti [Tue, 8 May 2012 09:56:46 +0000 (09:56 +0000)]
Added compare auxiliary machine for universal turing machine.

12 years agoprogress
Wilmer Ricciotti [Mon, 7 May 2012 15:34:16 +0000 (15:34 +0000)]
progress

12 years agoProve di terminazione
Andrea Asperti [Mon, 7 May 2012 13:13:32 +0000 (13:13 +0000)]
Prove di terminazione

12 years agoMore examples
Andrea Asperti [Mon, 7 May 2012 06:28:47 +0000 (06:28 +0000)]
More examples

12 years agostarl
Andrea Asperti [Mon, 7 May 2012 06:26:54 +0000 (06:26 +0000)]
starl

12 years agoForgotten in previous commit: move_char machines.
Wilmer Ricciotti [Fri, 4 May 2012 16:58:11 +0000 (16:58 +0000)]
Forgotten in previous commit: move_char machines.

12 years ago(no commit message)
Claudio Sacerdoti Coen [Fri, 4 May 2012 15:16:39 +0000 (15:16 +0000)]

12 years ago(no commit message)
Claudio Sacerdoti Coen [Fri, 4 May 2012 15:14:44 +0000 (15:14 +0000)]

12 years agoAdded a turing/universal directory for the universal turing machine (and
Wilmer Ricciotti [Fri, 4 May 2012 15:09:54 +0000 (15:09 +0000)]
Added a turing/universal directory for the universal turing machine (and
auxiliary definitions).
Added the definition of machine move_char (variant c) to be used in the
universal machine.
Small library refactoring.

12 years agoprogress
Wilmer Ricciotti [Fri, 4 May 2012 12:04:18 +0000 (12:04 +0000)]
progress

12 years agoSpeed up: moved a #ppterm inside the lazy it belongs to.
Claudio Sacerdoti Coen [Thu, 3 May 2012 19:26:39 +0000 (19:26 +0000)]
Speed up: moved a #ppterm inside the lazy it belongs to.

12 years agoprogress in while test machine
Wilmer Ricciotti [Thu, 3 May 2012 16:13:27 +0000 (16:13 +0000)]
progress in while test machine

12 years agoadditions in basic_2
Ferruccio Guidi [Thu, 3 May 2012 15:29:23 +0000 (15:29 +0000)]
additions in basic_2

12 years ago- more properties on lifting, slicing, delifting and thinning
Ferruccio Guidi [Thu, 3 May 2012 15:27:32 +0000 (15:27 +0000)]
- more properties on lifting, slicing, delifting and thinning

12 years agoprod fin set
Andrea Asperti [Thu, 3 May 2012 09:30:27 +0000 (09:30 +0000)]
prod fin set
-

12 years agobool and segments of natural numbers
Andrea Asperti [Thu, 3 May 2012 08:08:19 +0000 (08:08 +0000)]
bool and segments of natural numbers

12 years agoWhile semantics.
Wilmer Ricciotti [Wed, 2 May 2012 15:45:10 +0000 (15:45 +0000)]
While semantics.

12 years agosplit e merge
Andrea Asperti [Wed, 2 May 2012 13:10:30 +0000 (13:10 +0000)]
split e merge

12 years agoprogress
Andrea Asperti [Wed, 2 May 2012 12:00:00 +0000 (12:00 +0000)]
progress
-

12 years agowhile machine
Andrea Asperti [Wed, 2 May 2012 10:33:34 +0000 (10:33 +0000)]
while machine

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