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

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

Parent Directory Parent Directory | Revision Log Revision Log


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

Revision 3593 - (view) (download) (annotate) - [select for diffs]
Modified Tue Apr 30 00:41:41 2002 UTC (19 years, 1 month ago) by kopylov
File length: 11284 byte(s)
Diff to previous 3459
Change the documentation in czf_fol again (union -> +).
Also change the documentation for records.


Revision 3459 - (view) (download) (annotate) - [select for diffs]
Modified Tue Dec 4 02:49:30 2001 UTC (19 years, 6 months ago) by kopylov
File length: 11300 byte(s)
Diff to previous 3424
I define the Stack type as an example of
data structure defined with records.


Revision 3424 - (view) (download) (annotate) - [select for diffs]
Modified Mon Oct 22 21:05:57 2001 UTC (19 years, 8 months ago) by kopylov
File length: 10344 byte(s)
Diff to previous 3329
Added an example of mutually recursive functions based on records.


Revision 3329 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jul 13 21:34:19 2001 UTC (19 years, 11 months ago) by nogin
File length: 9205 byte(s)
Diff to previous 3298
I've removed old Itt_int* theories and switched all the ITT to Yegor's
new theories.


Revision 3298 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jun 25 01:34:52 2001 UTC (20 years ago) by kopylov
File length: 9203 byte(s)
Diff to previous 3281
- All rules in record theories are prooved (except some simple arith facts).

- Now progressT checks whether the assumptions are changed (not only the goal).

- Add a new operator tsquash{A}={Top|A}


Revision 3281 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jun 20 13:56:53 2001 UTC (20 years ago) by nogin
File length: 7177 byte(s)
Diff to previous 3276
The redundant "_resource" suffix should not be used in resource names.


Revision 3276 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jun 19 15:17:10 2001 UTC (20 years ago) by nogin
File length: 7330 byte(s)
Diff to previous 3274
Added support for the following syntax of resource improvement:
let resource name += expr
and
let resource name += [ expr1; expr2; ...; exprn ]


Revision 3274 - (view) (download) (annotate) - [select for diffs]
Modified Sun Jun 17 21:41:29 2001 UTC (20 years ago) by kopylov
File length: 7497 byte(s)
Diff to previous 3266
- Added tacticals whileProgressMT and untilFailMT

- Implemented dependend records

- Change a rule for depended intersection


Revision 3266 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jun 15 01:03:18 2001 UTC (20 years ago) by kopylov
File length: 7409 byte(s)
Diff to previous 3262
Start writing documentation for records.


Revision 3262 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jun 14 20:46:42 2001 UTC (20 years ago) by kopylov
File length: 4658 byte(s)
Diff to previous 3257
- More record theorems are proved

- I restored eta-reduction rule, which is valid (with correct mechanism
  for conditional rewrites)


Revision 3257 - (view) (download) (annotate) - [select for diffs]
Added Wed Jun 13 19:32:30 2001 UTC (20 years ago) by kopylov
File length: 4031 byte(s)
1. I added new primitive rules:
     Itt_struct.exchange
     Itt_pointwise.hypSubstPointwise
     Itt_pointwise.contextSubstPointwise

   The last two rules show the differences between pointwise and pairwise functionality.
   They are valid in pointwise functionality (as well as quoationtElimination2).

2. Itt_struct3 contains some rules that derived from these new ones.
   But thesd rules are valid in both functionalities.

3. I moved definition of natural numbers to a new theory Itt_nat.
   To prove induction for natural numbers one needs Itt_struct3.
   I almost proved it (leaving some simple arithmetic subgoals, that should
   be killed by arith)

4. I defined record type.
   Itt_record is a main theory of records.
   Itt_record_exm contains some examples.

5. I add a new conversion
        * applyAllC : conv list -> conv
   that applies all conversions to all subterms and a tactic
        * rwa : conv list -> int -> tactic
        = rw (applyAllC convs)


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