- predefined_virtuals: an addition
- lambda_delta: some notation changes

Progress.

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).

additions to basic_2

- lib: some additions
- lambda_delta: more properties on native type assignment
                change of notation for consand append

Sys.Break no longer captured in two places.

axiomatization of acc_if

Progress.

Progress in compare.ma (some machines have been moved to tests.ma and marks.ma)

progress in turing/universal/compare.ma

Added compare auxiliary machine for universal turing machine.

progress

Prove di terminazione

More examples

starl

Forgotten in previous commit: move_char machines.

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.

progress

Speed up: moved a #ppterm inside the lazy it belongs to.

progress in while test machine

additions in basic_2

- more properties on lifting, slicing, delifting and thinning

prod fin set
-

bool and segments of natural numbers

While semantics.

split e merge

progress
-

while machine

Added weak realizability.

Added wmono.

More proofs in if-then-else machine.

Le configurazioni sono definite non su macchine ma su stati.
Idem per alcune funzioni di lift.

Definition of accRealize

If machine

Monotape turing machines update.

more loop proofs

loop functions

loop functions

Mono tape turing machines

Extensions to finset (sum) and auxiliary lemmas.

- 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)

additions in basic_2

- lambda_delta: bug fix in static type assignment
                some theorems on delift and thin
- nat: eliminator for nat with "+1" rather than "S"

Update to universal turing machine (preliminaries).

More turing machines (still not compiling)

Started converting informal definition of the machines to matita code
(currently not compiling).

Added universal turing machines (only comments for now).

additions to basic_2

- lambda_delta: static type assignment is defined
- predefined_virtuals: some additions
- nat: we added a lemma

- update in basic_2

- firs theorems on native type assignment
- we removed iterated unfold on local environments
  since transitivity of this unfold is not needed so far

Fixed w.r.t. new yelp.

- milestone update in basic_2
- html bugfix in hand written web pages

- subject equivalence for atomic arity assignment completed!
- bug fix in partial unfold for local environments (nowthis relation
is confluent)

Definition of complexity

commit by user ricciott

commit by user

urgent partial commit ... to be fixed later ...

urgent partial commit ... to be fixed later ...

update in basic_2

- some work on context equivalence of atomic arity assignment

Added in basics
- vectors.ma
- finset.ma

Added turing

minor ntegrations in list,ma and listb.ma

Minor changes

More changes to the website (matitaweb).

Various updates to the (obsolete) website.

modifiche

Versione italiana

New home

Top picture

prova

Created a new directory for Matita1.0

additions to basic_2

- more on subject reduction of atomic arity assignment
- some results on context-sensitive equivalence of terms

manual commit

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.

additions in basic_2

- pts: we restored the former hierarchy
- nat: we added a missing lemma
- lambda_delta: subject reduction continues ...

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.

Matitaweb: Fixes a bug which prevented Mozilla from displaying long goals
correctly.

commit by user andrea

commit by user utente2

commit by user

commit by user ricciott

commit by user andrea

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).

additions to basic_2

- basics: bug fix in Conf3, it was not generic enough
- lambda_delta: subject reduction of static typestarted ...

update in basic_2 and apps_2

- 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

renaming completed

some renaming (ld_ prefix removed from file names)

some renaming: ld_ prefix removed

milestone update in basic_2!

- lambda_delta: strong normalization of simply typed terms closed!
- star.ma: transitive closure: support for reverse elimination

Manual commit (basics/core_notation.ma)

update in basic_2

property S2 of strongly normalizing terms proved!

- property S4 of strongly normalizing term proved!