]> matita.cs.unibo.it Git - helm.git/log
helm.git
11 years agoupdate in basic_2
Ferruccio Guidi [Fri, 4 Oct 2013 15:03:51 +0000 (15:03 +0000)]
update in basic_2

11 years agolenv refinement for native validity removed from big tree reduction
Ferruccio Guidi [Fri, 4 Oct 2013 15:02:46 +0000 (15:02 +0000)]
lenv refinement for native validity removed from big tree reduction

11 years agoupdate in basic_2
Ferruccio Guidi [Fri, 4 Oct 2013 13:37:34 +0000 (13:37 +0000)]
update in basic_2

11 years ago- degree assignment, static type assignment, iterated static type
Ferruccio Guidi [Fri, 4 Oct 2013 13:34:48 +0000 (13:34 +0000)]
- degree assignment, static type assignment, iterated static type
assignment and lenv refinement for native validity reaxiomatized to
move lsubsv_snv_trans out of the mutual induction for preservation
- minor stylistic improvements and Makefile bugfix

11 years agoAdds transformation of generic monotape machines into machines using a binary
Wilmer Ricciotti [Thu, 3 Oct 2013 15:07:11 +0000 (15:07 +0000)]
Adds transformation of generic monotape machines into machines using a binary
alphabet (first commit, doesn't typecheck)

11 years agoa vector of finsets is a finset (in progress)
Andrea Asperti [Wed, 2 Oct 2013 13:44:56 +0000 (13:44 +0000)]
a vector of finsets is a finset (in progress)

11 years agoprevious commit continued :)
Ferruccio Guidi [Sat, 7 Sep 2013 17:11:03 +0000 (17:11 +0000)]
previous commit continued :)

11 years agosupport for nat-labeled reflexive and transitive closure added to lambdadelta
Ferruccio Guidi [Sat, 7 Sep 2013 17:07:12 +0000 (17:07 +0000)]
support for nat-labeled reflexive and transitive closure added to lambdadelta

11 years ago- test.ma on the disambiguation bug moved to ONAG (just out of the way)
Ferruccio Guidi [Fri, 9 Aug 2013 20:06:52 +0000 (20:06 +0000)]
- test.ma on the disambiguation bug moved to ONAG (just out of the way)
- lambdadelta: updated interpretation descriptions fix the disambiguation bug

11 years ago- the example is now minimal so the bug is understood.
Ferruccio Guidi [Fri, 9 Aug 2013 18:20:26 +0000 (18:20 +0000)]
- the example is now minimal so the bug is understood.
  two interpretations of the same notation with the same description
  override eachother, so the description is not just informative :)
- more keywords added for highlighting

11 years ago- the example is smaller and really self-contained ...
Ferruccio Guidi [Fri, 9 Aug 2013 17:27:58 +0000 (17:27 +0000)]
- the example is smaller and really self-contained ...
- two keywords added for highlighting

11 years agoriduced example showing disambiguation bug ...
Ferruccio Guidi [Fri, 9 Aug 2013 16:13:09 +0000 (16:13 +0000)]
riduced example showing disambiguation bug ...

11 years ago- matitadep: new option -t to list the unreferenced sources
Ferruccio Guidi [Fri, 9 Aug 2013 14:43:14 +0000 (14:43 +0000)]
- matitadep: new option -t to list the unreferenced sources
- lambdadelta: Makefile update to use matitadep -t
               redundant dependecy removed in cl_weight
       test.ma: shows a bug in the disambiguation mechanism

11 years ago- we added nat-labeled reflexive and transitive closure (for use in lambdadelta)
Ferruccio Guidi [Fri, 9 Aug 2013 10:59:49 +0000 (10:59 +0000)]
- we added nat-labeled reflexive and transitive closure (for use in lambdadelta)
- stylistic improvements in list-labeled reflexive and transitive closure

11 years agomilestone in basic_2
Ferruccio Guidi [Wed, 7 Aug 2013 21:42:41 +0000 (21:42 +0000)]
milestone in basic_2

11 years agopassive support for global environments completed!
Ferruccio Guidi [Wed, 7 Aug 2013 21:38:40 +0000 (21:38 +0000)]
passive support for global environments completed!

11 years agopartial commit: "conversion" and "equivalence" components ...
Ferruccio Guidi [Wed, 7 Aug 2013 14:44:32 +0000 (14:44 +0000)]
partial commit: "conversion" and "equivalence" components ...

11 years agopartial commit: "computation" component ...
Ferruccio Guidi [Tue, 6 Aug 2013 16:40:51 +0000 (16:40 +0000)]
partial commit: "computation" component ...

11 years agopartial commit: "reduction" component
Ferruccio Guidi [Sat, 3 Aug 2013 14:37:51 +0000 (14:37 +0000)]
partial commit: "reduction" component

11 years agopartial commit: "unfold" component
Ferruccio Guidi [Thu, 1 Aug 2013 20:30:06 +0000 (20:30 +0000)]
partial commit: "unfold" component

11 years agopartial commit: "static" component ....
Ferruccio Guidi [Thu, 1 Aug 2013 15:05:48 +0000 (15:05 +0000)]
partial commit: "static" component ....

11 years agopartial commit: just the components before "static" ...
Ferruccio Guidi [Thu, 1 Aug 2013 12:32:09 +0000 (12:32 +0000)]
partial commit: just the components before "static" ...

11 years ago- the milestone was not reported on the web page!
Ferruccio Guidi [Sat, 27 Jul 2013 16:37:16 +0000 (16:37 +0000)]
- the milestone was not reported on the web page!
- we say on the web pages how nodes are counted

11 years agomilesone in basic_2!
Ferruccio Guidi [Sat, 27 Jul 2013 16:35:29 +0000 (16:35 +0000)]
milesone in basic_2!

11 years ago- probe: critical bug fixed (all objects were deleted due to wrong test)
Ferruccio Guidi [Sat, 27 Jul 2013 16:10:57 +0000 (16:10 +0000)]
- probe: critical bug fixed (all objects were deleted due to wrong test)
- lambdadelta: lenv refinement for atomic arity assignment updated,
               some renaming and notational change
reaxiomatization of beta-reduction complete! (milestone)

11 years agolambdadelta
Ferruccio Guidi [Fri, 26 Jul 2013 18:03:47 +0000 (18:03 +0000)]
lambdadelta
- we changed the beta-reductum to make reduction a special case of
  extended reduction, the lenv refinement for native validity was
  updated accordingly
- we parked restricted reduction, substitution and lenv refinement for
  static type assignment
- active notations are now one per file and are included by nead: this
  avoids time-wasting recompilations when notations are added, removed,
  or changed
- Makefile: some speed up, uses new version of mac, handles auxiliary
  xoa files that can be included by need to avoid time-wasting
  recompilations when xoa objects are added
mac
- now outputs the pages count
probe
- minor bug fix: exceptions during file removal where not cought

11 years agomilestone in basic_2
Ferruccio Guidi [Sat, 20 Jul 2013 22:12:29 +0000 (22:12 +0000)]
milestone in basic_2

11 years ago- new extendedd beta-reductum involving native type annotation
Ferruccio Guidi [Sat, 20 Jul 2013 22:10:11 +0000 (22:10 +0000)]
- new extendedd beta-reductum involving native type annotation
- extended strong normalization for simply typed terms (milestone)
- some renaming

11 years agopartial commit of the components before "conversion"
Ferruccio Guidi [Sat, 13 Jul 2013 15:08:58 +0000 (15:08 +0000)]
partial commit of the components before "conversion"
- some work on extended reduction and computation
- some renaming

11 years agoupdate in basic_2
Ferruccio Guidi [Thu, 20 Jun 2013 17:25:36 +0000 (17:25 +0000)]
update in basic_2

11 years ago- bug fix il ldrop (interesting), fsup, fsups
Ferruccio Guidi [Thu, 20 Jun 2013 17:23:20 +0000 (17:23 +0000)]
- bug fix il ldrop (interesting), fsup, fsups
- now fsupq is the reflexive closure of fsup, as expected
- some renaming

11 years ago- partial commit :(
Ferruccio Guidi [Wed, 19 Jun 2013 15:01:49 +0000 (15:01 +0000)]
- partial commit :(
  some work on supclosure and extended reduction ...

11 years agoupdate in basic_2
Ferruccio Guidi [Sat, 8 Jun 2013 20:22:59 +0000 (20:22 +0000)]
update in basic_2

11 years agomore results on extended reduction
Ferruccio Guidi [Sat, 8 Jun 2013 20:21:50 +0000 (20:21 +0000)]
more results on extended reduction

11 years agosome work on extended reduction ...
Ferruccio Guidi [Wed, 5 Jun 2013 21:54:08 +0000 (21:54 +0000)]
some work on extended reduction ...

11 years agoupdate in basic_2
Ferruccio Guidi [Mon, 3 Jun 2013 14:25:02 +0000 (14:25 +0000)]
update in basic_2

11 years agoredundant dependence removed
Ferruccio Guidi [Mon, 3 Jun 2013 13:58:42 +0000 (13:58 +0000)]
redundant dependence removed

11 years ago- a comment removed
Ferruccio Guidi [Mon, 3 Jun 2013 13:51:45 +0000 (13:51 +0000)]
- a comment removed

11 years ago- induction on supclosure replaces induction on weight for closures everywhere
Ferruccio Guidi [Mon, 3 Jun 2013 13:45:42 +0000 (13:45 +0000)]
- induction on supclosure replaces induction on weight for closures everywhere
- bug fix in csn_alt

11 years agoupdate in basic_2 and apps_2
Ferruccio Guidi [Sat, 1 Jun 2013 16:42:29 +0000 (16:42 +0000)]
update in basic_2 and apps_2

11 years ago- basic_2: induction for preservation results now uses supclosure
Ferruccio Guidi [Sat, 1 Jun 2013 14:27:30 +0000 (14:27 +0000)]
- basic_2: induction for preservation results now uses supclosure
relation rather than weight on closures
- app_2: "functional" component updated
- we park delifting substitution for now

11 years agoiteration.ma
Andrea Asperti [Fri, 31 May 2013 09:47:33 +0000 (09:47 +0000)]
iteration.ma

11 years agobounded quantifiers and pidgeon_hole
Andrea Asperti [Fri, 31 May 2013 09:41:17 +0000 (09:41 +0000)]
bounded quantifiers and pidgeon_hole

11 years agogap.ma
Andrea Asperti [Fri, 31 May 2013 09:39:54 +0000 (09:39 +0000)]
gap.ma

11 years agoNuovi files
matitaweb [Fri, 31 May 2013 09:36:04 +0000 (09:36 +0000)]
Nuovi files

11 years agocommit by user andrea
matitaweb [Thu, 30 May 2013 13:59:41 +0000 (13:59 +0000)]
commit by user andrea

11 years agocommit by user andrea
matitaweb [Thu, 30 May 2013 13:58:02 +0000 (13:58 +0000)]
commit by user andrea

11 years agocommit by user andrea
matitaweb [Wed, 29 May 2013 14:50:41 +0000 (14:50 +0000)]
commit by user andrea

11 years agoError to debug
Andrea Asperti [Tue, 28 May 2013 09:56:51 +0000 (09:56 +0000)]
Error to debug

11 years agoImproved version
Andrea Asperti [Fri, 17 May 2013 11:22:57 +0000 (11:22 +0000)]
Improved version

11 years agomore functions
Andrea Asperti [Fri, 17 May 2013 08:21:06 +0000 (08:21 +0000)]
more functions

11 years agopartial update in basic_2
Ferruccio Guidi [Thu, 16 May 2013 14:38:01 +0000 (14:38 +0000)]
partial update in basic_2

11 years ago- some renaming
Ferruccio Guidi [Thu, 16 May 2013 14:35:06 +0000 (14:35 +0000)]
- some renaming
- finally we issue the "dynamic" component

11 years agopartial commit of the "dynamic" component
Ferruccio Guidi [Mon, 13 May 2013 21:23:25 +0000 (21:23 +0000)]
partial commit of the "dynamic" component

11 years agopartial update in basic_2 ...
Ferruccio Guidi [Fri, 10 May 2013 16:19:46 +0000 (16:19 +0000)]
partial update in basic_2 ...

11 years ago- partial commit: we issue the "conversion" and "equivalence" components
Ferruccio Guidi [Fri, 10 May 2013 16:15:53 +0000 (16:15 +0000)]
- partial commit: we issue the "conversion" and "equivalence" components
- we park conversion and equivalence on local environments for the moment

11 years agopartial commit in basic_2
Ferruccio Guidi [Thu, 9 May 2013 20:55:35 +0000 (20:55 +0000)]
partial commit in basic_2

11 years agopartial commit: finaly we issue the "computation" component ...
Ferruccio Guidi [Thu, 9 May 2013 20:53:51 +0000 (20:53 +0000)]
partial commit: finaly we issue the "computation" component ...

11 years ago- partial commit: refactoring in the components before "computation"
Ferruccio Guidi [Tue, 7 May 2013 16:07:42 +0000 (16:07 +0000)]
- partial commit: refactoring in the components before "computation"

11 years agopartial update in basic_2
Ferruccio Guidi [Sun, 5 May 2013 18:25:54 +0000 (18:25 +0000)]
partial update in basic_2

11 years ago- partial commit (just the components before computation)
Ferruccio Guidi [Sun, 5 May 2013 18:16:14 +0000 (18:16 +0000)]
- partial commit (just the components before computation)
- we park head normal forms for the moment
- some refactoring

11 years agoreverse complexity
Andrea Asperti [Fri, 3 May 2013 06:51:37 +0000 (06:51 +0000)]
reverse complexity

11 years agoBumped to 0.99.2.
Claudio Sacerdoti Coen [Tue, 30 Apr 2013 17:05:53 +0000 (17:05 +0000)]
Bumped to 0.99.2.

11 years agoMissing include.
Claudio Sacerdoti Coen [Tue, 30 Apr 2013 17:05:36 +0000 (17:05 +0000)]
Missing include.

11 years agochapter9
Andrea Asperti [Tue, 30 Apr 2013 16:17:51 +0000 (16:17 +0000)]
chapter9

11 years agotutorial
Andrea Asperti [Tue, 30 Apr 2013 16:15:46 +0000 (16:15 +0000)]
tutorial

11 years agoOld version dropped.
Claudio Sacerdoti Coen [Tue, 30 Apr 2013 16:05:01 +0000 (16:05 +0000)]
Old version dropped.

11 years agoNew notation for congruence
Andrea Asperti [Tue, 30 Apr 2013 15:53:37 +0000 (15:53 +0000)]
New notation for congruence

11 years agoThis line, and those below, will be ignored--
Andrea Asperti [Tue, 30 Apr 2013 15:39:19 +0000 (15:39 +0000)]
This line, and those below, will be ignored--

M    chebyshev/chebyshev_psi.ma
D    chebyshev/chebyshev_B.ma

11 years agocommit by user ricciott
matitaweb [Tue, 30 Apr 2013 14:51:34 +0000 (14:51 +0000)]
commit by user ricciott

11 years agoA few integrations (closed an axiom in finset).
Andrea Asperti [Mon, 29 Apr 2013 09:57:24 +0000 (09:57 +0000)]
A few integrations (closed an axiom in finset).

11 years agocommit by user andrea
matitaweb [Sat, 27 Apr 2013 15:56:10 +0000 (15:56 +0000)]
commit by user andrea

11 years agocommit by user andrea
matitaweb [Sat, 27 Apr 2013 15:00:47 +0000 (15:00 +0000)]
commit by user andrea

11 years agocommit by user andrea
matitaweb [Sat, 27 Apr 2013 14:59:25 +0000 (14:59 +0000)]
commit by user andrea

11 years agocommit by user andrea
matitaweb [Sat, 27 Apr 2013 14:49:38 +0000 (14:49 +0000)]
commit by user andrea

11 years agocommit by user andrea
matitaweb [Fri, 26 Apr 2013 16:09:28 +0000 (16:09 +0000)]
commit by user andrea

11 years agoAn attempt at ostensiby named syntax.
Wilmer Ricciotti [Thu, 25 Apr 2013 07:15:53 +0000 (07:15 +0000)]
An attempt at ostensiby named syntax.

11 years agoupdate in basic_2
Ferruccio Guidi [Sun, 21 Apr 2013 15:53:55 +0000 (15:53 +0000)]
update in basic_2

11 years agoone file was missing
Ferruccio Guidi [Sun, 21 Apr 2013 15:52:11 +0000 (15:52 +0000)]
one file was missing

11 years ago- we commit the "reduction" component
Ferruccio Guidi [Sun, 21 Apr 2013 15:51:01 +0000 (15:51 +0000)]
- we commit the "reduction" component
- we park the focalized reduction for the moment
- some refactoring

11 years agoupdate in basic_2
Ferruccio Guidi [Sat, 20 Apr 2013 19:34:58 +0000 (19:34 +0000)]
update in basic_2

11 years agorefactoring should be completed now
Ferruccio Guidi [Sat, 20 Apr 2013 18:27:28 +0000 (18:27 +0000)]
refactoring should be completed now

11 years agorefactoring completed :)
Ferruccio Guidi [Sat, 20 Apr 2013 18:24:54 +0000 (18:24 +0000)]
refactoring completed :)

11 years ago- we are committing just the components before "reducibility"
Ferruccio Guidi [Sat, 20 Apr 2013 18:21:31 +0000 (18:21 +0000)]
- we are committing just the components before "reducibility"
- first definition of "unfold"
- notation bugfix
- some refactoring

11 years agocommit by user lroversi
matitaweb [Fri, 19 Apr 2013 18:38:02 +0000 (18:38 +0000)]
commit by user lroversi

11 years agocommit by user andrea
matitaweb [Wed, 17 Apr 2013 11:12:29 +0000 (11:12 +0000)]
commit by user andrea

11 years agoFixes a bug which caused Meta_not_found exceptions to be raised after qed-ing a
Wilmer Ricciotti [Wed, 17 Apr 2013 10:50:45 +0000 (10:50 +0000)]
Fixes a bug which caused Meta_not_found exceptions to be raised after qed-ing a
lemma with unskipped goals closed by side-effect.

11 years agomilestone update in basic_2!
Ferruccio Guidi [Tue, 16 Apr 2013 19:52:17 +0000 (19:52 +0000)]
milestone update in basic_2!

11 years ago- we commit just the components before "reducibility"
Ferruccio Guidi [Tue, 16 Apr 2013 19:45:41 +0000 (19:45 +0000)]
- we commit just the components before "reducibility"
- reaxiomatized substitution and reduction now commute with respect to
subclosure
- delift and thin removed for now

11 years agouncommited file found :)
Ferruccio Guidi [Mon, 15 Apr 2013 17:55:59 +0000 (17:55 +0000)]
uncommited file found :)

11 years agocommit by user andrea
matitaweb [Wed, 10 Apr 2013 11:44:22 +0000 (11:44 +0000)]
commit by user andrea

11 years agocommit by user andrea
matitaweb [Wed, 10 Apr 2013 11:43:43 +0000 (11:43 +0000)]
commit by user andrea

11 years agocommit by user andrea
matitaweb [Wed, 10 Apr 2013 11:32:54 +0000 (11:32 +0000)]
commit by user andrea

11 years agocommit by user andrea
matitaweb [Wed, 10 Apr 2013 10:01:59 +0000 (10:01 +0000)]
commit by user andrea

11 years agoFixes a bug that caused an assertion failure when no notation was defined.
Wilmer Ricciotti [Tue, 9 Apr 2013 13:41:15 +0000 (13:41 +0000)]
Fixes a bug that caused an assertion failure when no notation was defined.

11 years agoPatch by Paolo Tranquilli. It fixes the following problem: when a new
Claudio Sacerdoti Coen [Mon, 8 Apr 2013 12:20:15 +0000 (12:20 +0000)]
Patch by Paolo Tranquilli. It fixes the following problem: when a new
tab was openened, the interface got confused about which script was focused.
It did not save the previous focused script if it was at end of file and
it saved it instead when switching from the new tab. Other bugs could be related
to that.

11 years agocommit by user andrea
matitaweb [Mon, 8 Apr 2013 11:53:15 +0000 (11:53 +0000)]
commit by user andrea

11 years agoupdate in basic_2 and apps_2
Ferruccio Guidi [Sun, 7 Apr 2013 21:38:03 +0000 (21:38 +0000)]
update in basic_2 and apps_2

11 years ago- new component for restricted computation (delta, zeta and tau only)
Ferruccio Guidi [Sun, 7 Apr 2013 21:36:03 +0000 (21:36 +0000)]
- new component for restricted computation (delta, zeta and tau only)
- subclosure preseves native validity asexpected
- some renaming

11 years agoupdate in basic_2
Ferruccio Guidi [Fri, 5 Apr 2013 12:25:17 +0000 (12:25 +0000)]
update in basic_2