/[mojave]/metaprl/theories/itt/itt_comment.ml
ViewVC logotype

Log of /metaprl/theories/itt/itt_comment.ml

Parent Directory Parent Directory | Revision Log Revision Log


Sticky Revision:
(Current path doesn't exist after revision 7950)

Revision 3584 - (view) (download) (annotate) - [select for diffs]
Modified Thu Apr 25 15:28:40 2002 UTC (19 years, 1 month ago) by nogin
File length: 32352 byte(s)
Diff to previous 3325
- Added the comment module to the theories.pdf ("make latex").

- Added a hack allowing to override a theory display with another theory's
display. This is necessary for bootstrapping reasons - it allows one
to get a reasonable output of a theory (e.g. Comment) that is defined before
all essential display forms (e.g. the Summary ones) are there.

- Added debugging code to make it easier to find dforms that cause
zone begin/end mismatch (and used it to get rid of all
the "Unballanced buffer" warnings in "make latex").

- Minor dforms&comments updates.


Revision 3325 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jul 10 00:11:03 2001 UTC (19 years, 11 months ago) by nogin
File length: 32489 byte(s)
Diff to previous 3324
- Rewrote the Itt_esquash theory based on my "better_tt" ideas.
- Now esquash is a primitive operator and not a defined one.
- This change also broke a few FOL and CZF theories that relied
on a bunch of invalid rules that I had to remove from Itt_esquash.


Revision 3324 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jul 9 20:57:19 2001 UTC (19 years, 11 months ago) by nogin
File length: 32812 byte(s)
Diff to previous 3235
Numerous display form updates.


Revision 3235 - (view) (download) (annotate) - [select for diffs]
Modified Sun May 20 23:04:08 2001 UTC (20 years, 1 month ago) by nogin
File length: 32854 byte(s)
Diff to previous 3232
Display form fixes.

- TeX: all object-level terms (theorem statements, etc) are now typeset
in math mode.

- Tex: variable names are now parsed to detect indeces. In particular,
  'a1 will now be printed as a_{1} and 'a1_2 will be printed as a_{1,2}.

- Tex: `|' symbol in display forms is now always handled correctly.

- Numerous small fixes.


Revision 3232 - (view) (download) (annotate) - [select for diffs]
Modified Thu May 17 22:06:20 2001 UTC (20 years, 1 month ago) by nogin
File length: 33118 byte(s)
Diff to previous 3223
I joined Itt_hide and Itt_squash into a single theory - Itt_squash that deals
with both the meta-level squash operator (Base_trivial!squash{}) and the type
theory squash operator (Itt_squash!squash{'A}). This makes sense because
these two operators are almost exectly the same in nature except for oe
being a meta-level operator and another - an object-level one.

This commit also renames Itt_hide!hide into Itt_squash!squash. This means
that we now have two operators named "squash", however this should not cause
any confusion since all part of the system (including the parser and display
form mechanism) take into account the number of arguments.

Warning: This commit probably broke lots of proofs. I plan to fix that
after I have a chance to rewrite the squash theory a little better (for
now I just copied the one from Itt_hide). Hopefully, I should have it
done within a week.


Revision 3223 - (view) (download) (annotate) - [select for diffs]
Modified Tue May 8 23:59:11 2001 UTC (20 years, 1 month ago) by nogin
File length: 33111 byte(s)
Diff to previous 3058
Finally, I am able to commit what I was getting to
in all these commits over the last several days.

I changed the parser to index declared opnames by its "shape" -
last string of opname + parameter types + subterm arities
instead of just the last string (as it used to be). This means that
the parser now checks whether the usage of an opname corresponds
to its declaration. This allowed me to detect numerous typos in
display forms and even some rules and rewrites and, hopefully,
will prevent people from making such typos in the future.

This is only the first pass of the implementation. I still need to:
- make sure none of my fixes broke any display forms that used to work
  because of typos cancelling each other
- update the documentation
- implement checking of shapes on the opnames specified using the
  Module!name notation (currently no checking is done on such opnames)


Revision 3058 - (view) (download) (annotate) - [select for diffs]
Added Sun Sep 10 20:41:19 2000 UTC (20 years, 9 months ago) by jyh
File length: 33255 byte(s)
Last commit failed partway through...


This form allows you to request diffs between any two revisions of this file. For each of the two "sides" of the diff, enter a numeric revision.

  Diffs between and
  Type of Diff should be a

  ViewVC Help
Powered by ViewVC 1.1.26