]> matita.cs.unibo.it Git - helm.git/commitdiff
decentralizing core notation
authorFerruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
Thu, 29 Mar 2018 22:28:23 +0000 (00:28 +0200)
committerFerruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
Thu, 29 Mar 2018 22:28:23 +0000 (00:28 +0200)
centralized core notation (one single file) has two disadvantages:
- when some core notation is added the whole "world" must be recompiled
- unused core notation loaded in the parser gets in the way when defining contrib-specific notation
by defining core notation on a "one notation per file" basis:
+ every contrib file can load just the needed notation
+ sharing is possible as before in that two contrib files can load the same notation file

decentralalization will occur is stages:
this is the first stage meant to solve some issues in
+ lambdadelta (! blocked by fact)
+ certifiedRev (o{} blocked by compose, comprehension, singl, subset)


No differences found