]> matita.cs.unibo.it Git - helm.git/log
helm.git
2 years agoupdate in delayed_updating
Ferruccio Guidi [Sat, 21 May 2022 18:23:22 +0000 (20:23 +0200)]
update in delayed_updating

+ unwind completed with an important result on lift

2 years agoupdate in ground
Ferruccio Guidi [Fri, 20 May 2022 20:43:51 +0000 (22:43 +0200)]
update in ground

+ additions to lifts

2 years agoupdate in ground
Ferruccio Guidi [Thu, 19 May 2022 10:11:11 +0000 (12:11 +0200)]
update in ground

+ new notation for application of a relocation

2 years agoupdate in delayed_updating
Ferruccio Guidi [Tue, 17 May 2022 19:09:39 +0000 (21:09 +0200)]
update in delayed_updating

+ generic unwind meeds to be  even more generic

2 years agoupdate in delayed_updating
Ferruccio Guidi [Tue, 17 May 2022 15:51:39 +0000 (17:51 +0200)]
update in delayed_updating

+ generic unwind for path
+ some old files parked

2 years agoupdate in delayed_updating
Ferruccio Guidi [Mon, 9 May 2022 19:08:36 +0000 (21:08 +0200)]
update in delayed_updating

+ main function to locate the referred binder
+ update function for unfold

2 years agoupdate in delayed_updating
Ferruccio Guidi [Thu, 5 May 2022 12:15:52 +0000 (14:15 +0200)]
update in delayed_updating

+ notation for reversed path

2 years agoupdate in delayed_updating
Ferruccio Guidi [Tue, 3 May 2022 20:45:16 +0000 (22:45 +0200)]
update in delayed_updating

+ conflicts solved

2 years agoupdate in delayed_updating
Ferruccio Guidi [Tue, 3 May 2022 18:31:58 +0000 (20:31 +0200)]
update in delayed_updating

+ closed paths
+ updated notation for height
+ some parked files added

2 years agoupdate in delayed_updating
Ferruccio Guidi [Tue, 3 May 2022 17:46:49 +0000 (19:46 +0200)]
update in delayed_updating

+ some notation updated
+ some unused files removed

2 years agoupdate in delayed_updating
Ferruccio Guidi [Thu, 28 Apr 2022 15:34:11 +0000 (17:34 +0200)]
update in delayed_updating

+ alternative definition of unwind based on lift

2 years agoupdate in delayed updating
Ferruccio Guidi [Thu, 28 Apr 2022 12:29:08 +0000 (14:29 +0200)]
update in delayed updating

updated notation

2 years agoupdate in delayed updating
Ferruccio Guidi [Wed, 27 Apr 2022 17:41:11 +0000 (19:41 +0200)]
update in delayed updating

+ new version of lift
+ corrected and updated notation

2 years agoupdate in ground
Ferruccio Guidi [Wed, 27 Apr 2022 17:34:39 +0000 (19:34 +0200)]
update in ground

+ some addittions and corrections

2 years agoupdate un delayed updating
Ferruccio Guidi [Wed, 27 Apr 2022 17:24:30 +0000 (19:24 +0200)]
update un delayed updating

+ some parked files

2 years agoWIP in delayed_updating
Ferruccio Guidi [Mon, 28 Mar 2022 23:11:32 +0000 (01:11 +0200)]
WIP in delayed_updating

+ we re focusing on a special case of the main theorem

2 years agoupdate in delayed updating
Ferruccio Guidi [Sat, 26 Mar 2022 20:12:19 +0000 (21:12 +0100)]
update in delayed updating

+ additions to lift

2 years agoupdate in ground
Ferruccio Guidi [Sat, 26 Mar 2022 16:56:36 +0000 (17:56 +0100)]
update in ground

+ some additions and corrections

2 years agoupdate in delayed_updating
Ferruccio Guidi [Thu, 24 Mar 2022 20:08:45 +0000 (21:08 +0100)]
update in delayed_updating

+ lift
+ two versions of unwind
+ some renaming, additions and corrections

2 years agoupdate in delayed_updating
Ferruccio Guidi [Wed, 16 Mar 2022 21:41:40 +0000 (22:41 +0100)]
update in delayed_updating

+ some additions and corrections

2 years agoupdate in ground
Ferruccio Guidi [Wed, 16 Mar 2022 21:32:37 +0000 (22:32 +0100)]
update in ground

+ some additions

2 years agopartial update in delayed_updating
Ferruccio Guidi [Tue, 1 Mar 2022 00:14:15 +0000 (01:14 +0100)]
partial update in delayed_updating

+ WIP

2 years agoupdate in ground
Ferruccio Guidi [Tue, 1 Mar 2022 00:12:44 +0000 (01:12 +0100)]
update in ground

+ minor corrections and additions

2 years agoupdate in delayed_updating
Ferruccio Guidi [Wed, 16 Feb 2022 22:45:20 +0000 (23:45 +0100)]
update in delayed_updating

+ important additionsand corrections

2 years agoupdate in ground
Ferruccio Guidi [Wed, 16 Feb 2022 22:42:18 +0000 (23:42 +0100)]
update in ground

+ some additions and corrections

2 years agoupdate in delayed_updating
Ferruccio Guidi [Mon, 14 Feb 2022 23:23:15 +0000 (00:23 +0100)]
update in delayed_updating

+ update count for paths
+ minor additions and corrections

2 years agoupdate in ground
Ferruccio Guidi [Mon, 14 Feb 2022 23:21:15 +0000 (00:21 +0100)]
update in ground

+ additions to tr_compose

2 years agoupdate in delayed_updating
Ferruccio Guidi [Sun, 13 Feb 2022 19:16:56 +0000 (20:16 +0100)]
update in delayed_updating

+ WIP on dfr_lift_bi
+ minor corrections

2 years agoupdate in ground
Ferruccio Guidi [Sun, 13 Feb 2022 19:14:50 +0000 (20:14 +0100)]
update in ground

+ main commutation of tr_compose and tr_uni

2 years agoupdate in delayed_updating
Ferruccio Guidi [Thu, 10 Feb 2022 10:38:29 +0000 (11:38 +0100)]
update in delayed_updating

+ relationship between grafted trees and updating clarified in the case of interest so far

2 years agoupdate in delayed_updating
Ferruccio Guidi [Mon, 7 Feb 2022 22:49:05 +0000 (23:49 +0100)]
update in delayed_updating

+ WIP on updating grafted trees

2 years agoupdate in delayed-updating
Ferruccio Guidi [Thu, 3 Feb 2022 13:11:58 +0000 (14:11 +0100)]
update in delayed-updating

+ relationship between updating an grafted terms clarified
+ progress with dfr-lift_bi

2 years agoupdate in delayed updating
Ferruccio Guidi [Mon, 31 Jan 2022 21:51:55 +0000 (22:51 +0100)]
update in delayed updating

+ additions to lift
+ bugs fixed in dtr and itr

2 years agoupdate in ground
Ferruccio Guidi [Mon, 31 Jan 2022 21:50:04 +0000 (22:50 +0100)]
update in ground

+ additions to subsets

2 years agoupdate in delayed_updating
Ferruccio Guidi [Sun, 30 Jan 2022 17:51:41 +0000 (18:51 +0100)]
update in delayed_updating

+ additions to lift
+ bugs fixed in ifr

2 years agoupdate in ground
Ferruccio Guidi [Sat, 29 Jan 2022 22:39:01 +0000 (23:39 +0100)]
update in ground

+ additions to tr_compose

2 years agoupdate in ground
Ferruccio Guidi [Fri, 28 Jan 2022 22:24:01 +0000 (23:24 +0100)]
update in ground

+ additions to tr_compose

2 years agoupdate in delayed_updating
Ferruccio Guidi [Mon, 24 Jan 2022 23:30:11 +0000 (00:30 +0100)]
update in delayed_updating

+ bugs fixed in depth, dfr, ifr
+ WIP on dfr_lift_bi

2 years agoupdate un delayed_updating
Ferruccio Guidi [Sun, 23 Jan 2022 22:01:15 +0000 (23:01 +0100)]
update un delayed_updating

+ bugs fixed in dfr and ifr

2 years agoupdate in ground
Ferruccio Guidi [Sun, 23 Jan 2022 22:00:06 +0000 (23:00 +0100)]
update in ground

+ additions on tr_pap

2 years agoupdate in delayed_updating
Ferruccio Guidi [Sat, 22 Jan 2022 19:12:27 +0000 (20:12 +0100)]
update in delayed_updating

+ bugs fixed id dfr and ifr

2 years agoupdate in ground
Ferruccio Guidi [Sat, 22 Jan 2022 19:11:12 +0000 (20:11 +0100)]
update in ground

+ additions on tr_id

2 years agoupdate in delayed_updating
Ferruccio Guidi [Sat, 22 Jan 2022 00:35:11 +0000 (01:35 +0100)]
update in delayed_updating

+ mark label added
+ bugs fixed in depth and reduction
+ two notations changed

2 years agoupdate in delayed_updating
Ferruccio Guidi [Thu, 20 Jan 2022 19:48:22 +0000 (20:48 +0100)]
update in delayed_updating

+ a premise removed from lift_fsubst_sn
+ dfr and ifr restated to take equiprovability into account
+ notatation update for preterms

2 years agoupdate in ground
Ferruccio Guidi [Thu, 20 Jan 2022 19:42:34 +0000 (20:42 +0100)]
update in ground

+ advanced eliminators on lists

2 years agoupdate in delayed_updating
Ferruccio Guidi [Tue, 18 Jan 2022 21:46:48 +0000 (22:46 +0100)]
update in delayed_updating

+ commutation of lift and fsubst
+ preterms renamed as prototerms

2 years agoupdate in grafite parser
Ferruccio Guidi [Tue, 18 Jan 2022 17:50:48 +0000 (18:50 +0100)]
update in grafite parser

+ parameter notation in record fields

2 years agoupdate in ground
Ferruccio Guidi [Tue, 18 Jan 2022 15:52:11 +0000 (16:52 +0100)]
update in ground

+ WIP on subsets

2 years agoupdate in delayed_updating
Ferruccio Guidi [Mon, 10 Jan 2022 15:49:52 +0000 (16:49 +0100)]
update in delayed_updating

+ proper condition for path
+ relation between lift and append proved

2 years agoupdate in delayed updating
Ferruccio Guidi [Mon, 10 Jan 2022 11:55:35 +0000 (12:55 +0100)]
update in delayed updating

+ notation for "proper element"
+ bug fixed ub the notation of predicates

2 years agoupdate in lib
Ferruccio Guidi [Sat, 8 Jan 2022 21:24:10 +0000 (22:24 +0100)]
update in lib

+ notation for card decentralized

2 years agoupdate in ground and delayed updating
Ferruccio Guidi [Sat, 8 Jan 2022 20:09:45 +0000 (21:09 +0100)]
update in ground and delayed updating

+ notation at level 75 moved at level 70
+ dfr, ifr: path depth was not considered

2 years agoupdate in delayed_updating
Ferruccio Guidi [Tue, 4 Jan 2022 15:48:03 +0000 (16:48 +0100)]
update in delayed_updating

+ improved lift

2 years agoupdate in delayed_updating
Ferruccio Guidi [Tue, 4 Jan 2022 12:09:51 +0000 (13:09 +0100)]
update in delayed_updating

+ immediate reduction defined
+ some lemmas with lift simplified

2 years agoupdate in delayed updating
Ferruccio Guidi [Sun, 2 Jan 2022 18:07:48 +0000 (19:07 +0100)]
update in delayed updating

+ some properties of lift

2 years agoupdate in ground, static_2 and apps_2
Ferruccio Guidi [Thu, 30 Dec 2021 12:24:12 +0000 (13:24 +0100)]
update in ground, static_2 and apps_2

+ updated notation for extensional equality

2 years agoupdate in delayed_updating
Ferruccio Guidi [Mon, 27 Dec 2021 23:38:37 +0000 (00:38 +0100)]
update in delayed_updating

+ updated notation for lists
+ WIP on lift

2 years agoupdate in ground, basic_2A and apps_2
Ferruccio Guidi [Sat, 25 Dec 2021 15:40:06 +0000 (16:40 +0100)]
update in ground, basic_2A and apps_2

+ notation for lists: fixed and updated

2 years agoupdate in ground
Ferruccio Guidi [Fri, 24 Dec 2021 09:52:38 +0000 (10:52 +0100)]
update in ground

+ uniform total relocations

2 years agoupdate in delayed updating
Ferruccio Guidi [Fri, 24 Dec 2021 09:50:41 +0000 (10:50 +0100)]
update in delayed updating

+ delayed focalized reduction

2 years agoupdate in ground
Ferruccio Guidi [Mon, 20 Dec 2021 18:08:34 +0000 (19:08 +0100)]
update in ground

+ composition for total relocation maps

2 years agoMerge branch 'master' of ssh://matita.cs.unibo.it:/srv/git/helm
Ferruccio Guidi [Sat, 18 Dec 2021 22:43:24 +0000 (23:43 +0100)]
Merge branch 'master' of ssh://matita.cs.unibo.it:/srv/git/helm

2 years agoupdate in ground
Ferruccio Guidi [Sat, 18 Dec 2021 22:42:38 +0000 (23:42 +0100)]
update in ground

+ positive application for total relocation maps completed

2 years agoupdate in delayed_updating
Ferruccio Guidi [Sat, 11 Dec 2021 21:17:15 +0000 (22:17 +0100)]
update in delayed_updating

+ terms are defined modulo logical equivalence

2 years agoupdate in ground
Ferruccio Guidi [Fri, 10 Dec 2021 23:23:33 +0000 (00:23 +0100)]
update in ground

+ basic support for subsets as predicates

2 years agoupdate in delayed updating
Ferruccio Guidi [Fri, 10 Dec 2021 15:49:53 +0000 (16:49 +0100)]
update in delayed updating

+ WIP on dephi
+ some renaming
+ subset notation improved

2 years agoupdate in delayed_updating
Ferruccio Guidi [Mon, 6 Dec 2021 19:45:59 +0000 (20:45 +0100)]
update in delayed_updating

+ wip on predicate for bdd terms
+ updated notation
+ additions to lists

2 years agoupdate in ground
Ferruccio Guidi [Sat, 4 Dec 2021 16:43:16 +0000 (17:43 +0100)]
update in ground

+ updated notation and terminology for lists

2 years agoupdate in ground
Ferruccio Guidi [Thu, 2 Dec 2021 21:45:57 +0000 (22:45 +0100)]
update in ground

+ additions and corrections on lists

2 years agoupdate in ground
Ferruccio Guidi [Thu, 2 Dec 2021 16:31:43 +0000 (17:31 +0100)]
update in ground

+ advances on total redlocation

2 years agocontribution on delayed updating begins
Ferruccio Guidi [Tue, 30 Nov 2021 16:38:07 +0000 (17:38 +0100)]
contribution on delayed updating begins

we place it here for convenience

2 years agoupdate in ground
Ferruccio Guidi [Tue, 30 Nov 2021 16:31:19 +0000 (17:31 +0100)]
update in ground

+ total relocation begins

2 years agoMerge branch 'master' of ssh://matita.cs.unibo.it:/srv/git/helm
Ferruccio Guidi [Tue, 30 Nov 2021 16:15:34 +0000 (17:15 +0100)]
Merge branch 'master' of ssh://matita.cs.unibo.it:/srv/git/helm

2 years agoλδ web site update
Ferruccio Guidi [Tue, 30 Nov 2021 16:14:14 +0000 (17:14 +0100)]
λδ web site update

+ updated bibliography

3 years agoupdate in ground static_2 basic_2 apps_2
Ferruccio Guidi [Fri, 29 Oct 2021 18:24:59 +0000 (20:24 +0200)]
update in ground static_2 basic_2 apps_2

+ two sets of bold parentheses were used. now just one

3 years agoupdate in ground
Ferruccio Guidi [Fri, 29 Oct 2021 18:11:28 +0000 (20:11 +0200)]
update in ground

+ total relocation restarted

3 years agopartial update in static_2
Ferruccio Guidi [Thu, 28 Oct 2021 14:42:33 +0000 (16:42 +0200)]
partial update in static_2

+ propagation of ground library in static_2/relocation begins
+ additions in ground

3 years agopartial update in static_2
Ferruccio Guidi [Mon, 18 Oct 2021 19:04:56 +0000 (21:04 +0200)]
partial update in static_2

+ ground library propagated in static/syntax
+ additions in ground

3 years agopartial update in static_2
Ferruccio Guidi [Mon, 11 Oct 2021 11:51:08 +0000 (13:51 +0200)]
partial update in static_2

+ propagating the ground library
+ one addition in ground

3 years agoupdate in ground
Ferruccio Guidi [Tue, 5 Oct 2021 22:53:00 +0000 (00:53 +0200)]
update in ground

+ minor bug fixed in a notation

3 years agopartial commit in static_2
Ferruccio Guidi [Tue, 5 Oct 2021 22:51:38 +0000 (00:51 +0200)]
partial commit in static_2

propagating the new ground library to static_2 begins

3 years agoupdate in ground
Ferruccio Guidi [Tue, 5 Oct 2021 22:47:56 +0000 (00:47 +0200)]
update in ground

+ one lemma was missing

3 years agoupdate in ground
Ferruccio Guidi [Mon, 4 Oct 2021 21:37:42 +0000 (23:37 +0200)]
update in ground

+ bug fixed in the notation of exp
+ minor bugs fixed

3 years agoupdate in ground
Ferruccio Guidi [Mon, 4 Oct 2021 16:03:25 +0000 (18:03 +0200)]
update in ground

+ some renaming

3 years agoupdate in ground
Ferruccio Guidi [Thu, 30 Sep 2021 18:16:10 +0000 (20:16 +0200)]
update in ground

+ new notation for head and tail

3 years agoupdate in ground and static_2
Ferruccio Guidi [Tue, 29 Jun 2021 16:31:37 +0000 (18:31 +0200)]
update in ground and static_2

+ notation update for tail function
+ predefined virtuals: one symbol added

3 years agoupdate in alpha_1
Ferruccio Guidi [Thu, 17 Jun 2021 11:50:05 +0000 (13:50 +0200)]
update in alpha_1

+ type of terms redefined
+ Makefile added to lambdadelta/bin
+ a correction static_2/syntax/term.ma

3 years agoλδ site update
Ferruccio Guidi [Mon, 14 Jun 2021 14:28:21 +0000 (16:28 +0200)]
λδ site update

+ one citation added to home page
+ one bug fixed in xhtbl.ml
+ ome comment added in gcp_cr.ma

3 years agoupdate in ground
Ferruccio Guidi [Sat, 29 May 2021 17:46:15 +0000 (19:46 +0200)]
update in ground

+ comments restyled

3 years agoλδ site update
Ferruccio Guidi [Sat, 29 May 2021 16:56:27 +0000 (18:56 +0200)]
λδ site update

+ ground and documentation

3 years agoprobe
Ferruccio Guidi [Sat, 29 May 2021 12:18:10 +0000 (14:18 +0200)]
probe

+ improved error handling

3 years agonCicLibrary
Ferruccio Guidi [Sat, 29 May 2021 08:43:47 +0000 (10:43 +0200)]
nCicLibrary

+ config flag added to emove old objects before storing new ones
  I don't even rememberwhy thisisnot done by default

3 years agoupdate in ground
Ferruccio Guidi [Sat, 29 May 2021 08:40:29 +0000 (10:40 +0200)]
update in ground

+ some renaming

3 years agocic notation parser
Ferruccio Guidi [Fri, 28 May 2021 22:47:00 +0000 (00:47 +0200)]
cic notation parser

syntax of constructors updated to match syntax of definitions

3 years agomilestone update in ground
Ferruccio Guidi [Fri, 28 May 2021 22:42:43 +0000 (00:42 +0200)]
milestone update in ground

+ generic relocation maps are now streams of booleans
+ some renaming and restyling
+ operator precedence more uniform
+ recomm updated for relocation

3 years agografite parser updated
Ferruccio Guidi [Thu, 18 Mar 2021 14:10:29 +0000 (15:10 +0100)]
grafite parser updated

+ syntax for parameters added to constructors
  as it was done with definitions some time ago

3 years agopropagating the arithmetics library, partial commit
Ferruccio Guidi [Mon, 15 Mar 2021 12:10:02 +0000 (13:10 +0100)]
propagating the arithmetics library, partial commit

+ relocation updated and ported (de Bruijn indexes now start at 1)
+ recomm updated to generate substitution files
+ results on positive integers added to arith
+ some corrections

3 years agoupdate in ground
Ferruccio Guidi [Sun, 28 Feb 2021 21:32:01 +0000 (22:32 +0100)]
update in ground

+ notation restyled

3 years agoupdate in ground
Ferruccio Guidi [Sun, 28 Feb 2021 19:54:43 +0000 (20:54 +0100)]
update in ground

+ xoa restyled
+ missing files committed

3 years agoupdate in gruound
Ferruccio Guidi [Sun, 28 Feb 2021 19:38:50 +0000 (20:38 +0100)]
update in gruound

+ library refactored and restyled
+ recomm updated