/[mojave]/metaprl/theories/itt
ViewVC logotype

Index of /metaprl/theories/itt

Files shown:176
Directory revision: 3584 (of 13286)
Sticky Revision:


File Rev. Age Author Last log entry
 Parent Directory        
.cprc  2032  24 years  jyh   This is the initial checkin of Nuprl-Light. I am porting the editor, so it is no…
.ispell_english  3124  20 years  nogin   Spelling changes. For best results, upgrade to http://www.cs.cornell.edu/nogin/R
Conscript  3410  19 years  nogin   - Merged the Ocaml 3.02 changes - Now http server is compiled in by default, bu…
Makefile  3347  20 years  nogin   I rewrote itt_collection using my "better_tt" ideas and proved all the theorems …
ctt_markov.ml  3281  20 years  nogin   The redundant "_resource" suffix should not be used in resource names.
ctt_markov.mli  3246  20 years  kopylov   - The theory ctt_markov (Constructive type theory with Markov Principle) is ad…
ctt_markov.prla  3331  20 years  nogin   - The Itt_quotient theory is now a theory of _intensional_ quotient type (one ca…
itt_atom.ml  3281  20 years  nogin   The redundant "_resource" suffix should not be used in resource names.
itt_atom.mli  3140  20 years  kopylov   For now 'a~'b produces Itt_squiggle!sqeq{'a;'b} rather then Perv!rewrite. I do…
itt_atom_bool.ml  3382  19 years  emre   Added reduce_eq_atom to the reduce resource.
itt_atom_bool.mli  2743  22 years  jyh   This is a major release; I bumped the release number to 0.6. WARNING: There are …
itt_bisect.ml  3319  20 years  kopylov   - Changed intro rule for the set type according to Alexey's beter_itt. - Proved…
itt_bisect.mli  3056  20 years  cwitty   Started changing declare/prim_rw to define (as in TODO 2.01.2). Also fixed an un…
itt_bisect.prla  3309  20 years  kopylov   Fixed some proofs.
itt_bool.ml  3584  19 years  nogin   - Added the comment module to the theories.pdf ("make latex"). - Added a hack a…
itt_bool.mli  3329  20 years  nogin   I've removed old Itt_int* theories and switched all the ITT to Yegor's new theor…
itt_bool.prla  3343  20 years  nogin   Itt_fset is finally complete!
itt_bugs.ml  3300  20 years  kopylov   - I moved the rule quotientElimination2 to the Itt_pointwise2, since it is vali…
itt_bugs.mli  3300  20 years  kopylov   - I moved the rule quotientElimination2 to the Itt_pointwise2, since it is vali…
itt_bugs.prla  3329  20 years  nogin   I've removed old Itt_int* theories and switched all the ITT to Yegor's new theor…
itt_bunion.ml  3307  20 years  kopylov   - added rules applyEquality to intro resource - many rules (e.g. letT and elimi…
itt_bunion.mli  3056  20 years  cwitty   Started changing declare/prim_rw to define (as in TODO 2.01.2). Also fixed an un…
itt_bunion.prla  3300  20 years  kopylov   - I moved the rule quotientElimination2 to the Itt_pointwise2, since it is vali…
itt_collection.ml  3347  20 years  nogin   I rewrote itt_collection using my "better_tt" ideas and proved all the theorems …
itt_collection.mli  3347  20 years  nogin   I rewrote itt_collection using my "better_tt" ideas and proved all the theorems …
itt_collection.prla  3347  20 years  nogin   I rewrote itt_collection using my "better_tt" ideas and proved all the theorems …
itt_comment.ml  3584  19 years  nogin   - Added the comment module to the theories.pdf ("make latex"). - Added a hack a…
itt_comment.mli  3325  20 years  nogin   - Rewrote the Itt_esquash theory based on my "better_tt" ideas. - Now esquash is…
itt_decidable.ml  3344  20 years  nogin   - created a tcaT tactic that is equivalent to tryT (completeT autoT) - created a…
itt_decidable.mli  3329  20 years  nogin   I've removed old Itt_int* theories and switched all the ITT to Yegor's new theor…
itt_decidable.prla  3419  19 years  nogin   - I got rid of "MAKE_JOBS" variable in mk/config. If you want "make" to keep run…
itt_derive.ml  3139  20 years  nogin   I moved the bind operator from ITT to the Perv module. This makes sense because …
itt_derive.mli  2743  22 years  jyh   This is a major release; I bumped the release number to 0.6. WARNING: There are …
itt_derive.prla  3139  20 years  nogin   I moved the bind operator from ITT to the Perv module. This makes sense because …
itt_dfun.ml  3525  19 years  nogin   Minor ITT clean-up: - No need to use addHiddenLabelT when annotation on a rule w…
itt_dfun.mli  3346  20 years  nogin   Added subtypeT function: subtypeT <<A>> replaces a conclusion of the form <<t1 =…
itt_dfun.prla  3272  20 years  nogin   Wrote Itt_struct.nthAssumT that is very similar to base theory nthAssumT, but ca…
itt_disect.ml  3525  19 years  nogin   Minor ITT clean-up: - No need to use addHiddenLabelT when annotation on a rule w…
itt_disect.mli  3303  20 years  kopylov   Simplify primitive rules and improve tactics for elimination of intersection typ…
itt_disect.prla  3463  19 years  nogin   Fixed bug #10 - now the term_match_table fall-back mechanism is more complete. T…
itt_dprod.ml  3525  19 years  nogin   Minor ITT clean-up: - No need to use addHiddenLabelT when annotation on a rule w…
itt_dprod.mli  3334  20 years  nogin   When a bound variable already exists in the goal, it should not be supplied in t…
itt_dprod.prla  3279  20 years  nogin   - Renamed andthenC -> thenC - Added byDefT : conv -> tactic - Proved rewrites in…
itt_dprod_imp.ml  3281  20 years  nogin   The redundant "_resource" suffix should not be used in resource names.
itt_dprod_imp.mli  2912  21 years  jyh   Most of the theories in Itt now expand without errors. One exception is Itt_fset…
itt_dprod_imp.prla  3344  20 years  nogin   - created a tcaT tactic that is equivalent to tryT (completeT autoT) - created a…
itt_equal.ml  3343  20 years  nogin   Itt_fset is finally complete!
itt_equal.mli  3326  20 years  nogin   - trivialT can now do equalRefT and equalSymT when necessary to match the conclu…
itt_equal.prla  3326  20 years  nogin   - trivialT can now do equalRefT and equalSymT when necessary to match the conclu…
itt_esquash.ml  3524  19 years  nogin   esquash_mem does not have to be primitive, it follows directly from esquash_elim…
itt_esquash.mli  3325  20 years  nogin   - Rewrote the Itt_esquash theory based on my "better_tt" ideas. - Now esquash is…
itt_esquash.prla  3524  19 years  nogin   esquash_mem does not have to be primitive, it follows directly from esquash_elim…
itt_eta.ml  3323  20 years  kopylov   Fix some proofs
itt_eta.mli  3323  20 years  kopylov   Fix some proofs
itt_ext_equal.ml  3307  20 years  kopylov   - added rules applyEquality to intro resource - many rules (e.g. letT and elimi…
itt_ext_equal.mli  2494  22 years  jyh   I changed all the obvious places of Nuprl-Light, NL, nl, or any other instance t…
itt_ext_equal.prla  3309  20 years  kopylov   Fixed some proofs.
itt_fset.ml  3344  20 years  nogin   - created a tcaT tactic that is equivalent to tryT (completeT autoT) - created a…
itt_fset.mli  3340  20 years  nogin   More itt_fset fixes.
itt_fset.prla  3345  20 years  nogin   - Added a new tactic copyHypT for copying hypotheses (useful in elimination rule…
itt_fun.ml  3347  20 years  nogin   I rewrote itt_collection using my "better_tt" ideas and proved all the theorems …
itt_fun.mli  3058  20 years  jyh   Last commit failed partway through...
itt_fun.prla  3346  20 years  nogin   Added subtypeT function: subtypeT <<A>> replaces a conclusion of the form <<t1 =…
itt_int_arith.ml  3542  19 years  yegor   Arithmetic relations in conclusion is also processed now. TODO: - "bug"(a>=b & a…
itt_int_arith.mli  3542  19 years  yegor   Arithmetic relations in conclusion is also processed now. TODO: - "bug"(a>=b & a…
itt_int_arith.prla  3542  19 years  yegor   Arithmetic relations in conclusion is also processed now. TODO: - "bug"(a>=b & a…
itt_int_base.ml  3352  19 years  nogin   - Made sure conditional rewrites are added to toploop the same way the normal ru…
itt_int_base.mli  3352  19 years  nogin   - Made sure conditional rewrites are added to toploop the same way the normal ru…
itt_int_base.prla  3419  19 years  nogin   - I got rid of "MAKE_JOBS" variable in mk/config. If you want "make" to keep run…
itt_int_ext.ml  3442  19 years  yegor   Itt_int_ext: more conversions added to reduce resource Itt_int_arih: first work…
itt_int_ext.mli  3442  19 years  yegor   Itt_int_ext: more conversions added to reduce resource Itt_int_arih: first work…
itt_int_ext.prla  3279  20 years  nogin   - Renamed andthenC -> thenC - Added byDefT : conv -> tactic - Proved rewrites in…
itt_inv_typing.ml  3318  20 years  kopylov   - Fixed some bugs in Itt_w: (a) The rule ruduce_tree_eta was unsound (we could…
itt_inv_typing.mli  3277  20 years  kopylov   - New tacticals onAllAssumT : (int -> tactic) -> tactic onAllMAssumT : (…
itt_isect.ml  3525  19 years  nogin   Minor ITT clean-up: - No need to use addHiddenLabelT when annotation on a rule w…
itt_isect.mli  3303  20 years  kopylov   Simplify primitive rules and improve tactics for elimination of intersection typ…
itt_isect.prla  3344  20 years  nogin   - created a tcaT tactic that is equivalent to tryT (completeT autoT) - created a…
itt_list.ml  3525  19 years  nogin   Minor ITT clean-up: - No need to use addHiddenLabelT when annotation on a rule w…
itt_list.mli  3342  20 years  nogin   - Proved list cons-cons equality elimination. - More itt_fset proofs.
itt_list.prla  3342  20 years  nogin   - Proved list cons-cons equality elimination. - More itt_fset proofs.
itt_list2.ml  3584  19 years  nogin   - Added the comment module to the theories.pdf ("make latex"). - Added a hack a…
itt_list2.mli  3056  20 years  cwitty   Started changing declare/prim_rw to define (as in TODO 2.01.2). Also fixed an un…
itt_list2.prla  3344  20 years  nogin   - created a tcaT tactic that is equivalent to tryT (completeT autoT) - created a…
itt_logic.ml  3584  19 years  nogin   - Added the comment module to the theories.pdf ("make latex"). - Added a hack a…
itt_logic.mli  3347  20 years  nogin   I rewrote itt_collection using my "better_tt" ideas and proved all the theorems …
itt_logic.prla  3347  20 years  nogin   I rewrote itt_collection using my "better_tt" ideas and proved all the theorems …
itt_nat.ml  3298  20 years  kopylov   - All rules in record theories are prooved (except some simple arith facts). - …
itt_nat.mli  3298  20 years  kopylov   - All rules in record theories are prooved (except some simple arith facts). - …
itt_nat.prla  3272  20 years  nogin   Wrote Itt_struct.nthAssumT that is very similar to base theory nthAssumT, but ca…
itt_pointwise.ml  3257  20 years  kopylov   1. I added new primitive rules: Itt_struct.exchange Itt_pointwise.hypS…
itt_pointwise.mli  3257  20 years  kopylov   1. I added new primitive rules: Itt_struct.exchange Itt_pointwise.hypS…
itt_pointwise.prla  3257  20 years  kopylov   1. I added new primitive rules: Itt_struct.exchange Itt_pointwise.hypS…
itt_pointwise2.ml  3300  20 years  kopylov   - I moved the rule quotientElimination2 to the Itt_pointwise2, since it is vali…
itt_pointwise2.mli  3300  20 years  kopylov   - I moved the rule quotientElimination2 to the Itt_pointwise2, since it is vali…
itt_pointwise2.prla  3333  20 years  nogin   When eliminating a quotient hyp, dT will now use a simplier rule (and use thinT …
itt_prec.ml  3318  20 years  kopylov   - Fixed some bugs in Itt_w: (a) The rule ruduce_tree_eta was unsound (we could…
itt_prec.mli  2674  22 years  nogin   I removed @ from the parameter syntax for meta-parameters. Now [xxx:s] is parsed…
itt_prod.ml  3525  19 years  nogin   Minor ITT clean-up: - No need to use addHiddenLabelT when annotation on a rule w…
itt_prod.mli  3334  20 years  nogin   When a bound variable already exists in the goal, it should not be supplied in t…
itt_prod.prla  3272  20 years  nogin   Wrote Itt_struct.nthAssumT that is very similar to base theory nthAssumT, but ca…
itt_prop_decide.ml  3279  20 years  nogin   - Renamed andthenC -> thenC - Added byDefT : conv -> tactic - Proved rewrites in…
itt_prop_decide.mli  2743  22 years  jyh   This is a major release; I bumped the release number to 0.6. WARNING: There are …
itt_prop_decide.prla  3279  20 years  nogin   - Renamed andthenC -> thenC - Added byDefT : conv -> tactic - Proved rewrites in…
itt_quotient.ml  3347  20 years  nogin   I rewrote itt_collection using my "better_tt" ideas and proved all the theorems …
itt_quotient.mli  3347  20 years  nogin   I rewrote itt_collection using my "better_tt" ideas and proved all the theorems …
itt_quotient.prla  3333  20 years  nogin   When eliminating a quotient hyp, dT will now use a simplier rule (and use thinT …
itt_record.ml  3315  20 years  nogin   I have changed the way autoT works. Now autoT and trivialT share the same auto_…
itt_record.mli  3298  20 years  kopylov   - All rules in record theories are prooved (except some simple arith facts). - …
itt_record.prla  3419  19 years  nogin   - I got rid of "MAKE_JOBS" variable in mk/config. If you want "make" to keep run…
itt_record0.ml  3298  20 years  kopylov   - All rules in record theories are prooved (except some simple arith facts). - …
itt_record0.mli  3298  20 years  kopylov   - All rules in record theories are prooved (except some simple arith facts). - …
itt_record0.prla  3317  20 years  kopylov   Fixed two proofs
itt_record_exm.ml  3459  19 years  kopylov   I define the Stack type as an example of data structure defined with records.
itt_record_exm.mli  3424  19 years  kopylov   Added an example of mutually recursive functions based on records.
itt_record_exm.prla  3459  19 years  kopylov   I define the Stack type as an example of data structure defined with records.
itt_record_label.ml  3298  20 years  kopylov   - All rules in record theories are prooved (except some simple arith facts). - …
itt_record_label.mli  3298  20 years  kopylov   - All rules in record theories are prooved (except some simple arith facts). - …
itt_record_label.prla  3298  20 years  kopylov   - All rules in record theories are prooved (except some simple arith facts). - …
itt_record_label0.ml  3334  20 years  nogin   When a bound variable already exists in the goal, it should not be supplied in t…
itt_record_label0.mli  3298  20 years  kopylov   - All rules in record theories are prooved (except some simple arith facts). - …
itt_record_label0.prla  3298  20 years  kopylov   - All rules in record theories are prooved (except some simple arith facts). - …
itt_rfun.ml  3584  19 years  nogin   - Added the comment module to the theories.pdf ("make latex"). - Added a hack a…
itt_rfun.mli  3223  20 years  nogin   Finally, I am able to commit what I was getting to in all these commits over the…
itt_rfun.prla  3272  20 years  nogin   Wrote Itt_struct.nthAssumT that is very similar to base theory nthAssumT, but ca…
itt_set.ml  3325  20 years  nogin   - Rewrote the Itt_esquash theory based on my "better_tt" ideas. - Now esquash is…
itt_set.mli  3319  20 years  kopylov   - Changed intro rule for the set type according to Alexey's beter_itt. - Proved…
itt_sort.ml  3385  19 years  nogin   Improved the demo theory.
itt_sort.mli  3056  20 years  cwitty   Started changing declare/prim_rw to define (as in TODO 2.01.2). Also fixed an un…
itt_sort.prla  3385  19 years  nogin   Improved the demo theory.
itt_squash.ml  3444  19 years  nogin   Code cleanup: I looked (using the code I've put into macro.ml) for places where…
itt_squash.mli  3305  20 years  nogin   Moved nthAssumT from Itt_struct to Itt_squash and made it do sequent squashing/u…
itt_squash.prla  3315  20 years  nogin   I have changed the way autoT works. Now autoT and trivialT share the same auto_…
itt_squiggle.ml  3292  20 years  nogin   *** IMPORTANT: before doing "cvs update" see warning below *** This commit impl…
itt_squiggle.mli  3257  20 years  kopylov   1. I added new primitive rules: Itt_struct.exchange Itt_pointwise.hypS…
itt_squiggle.prla  3139  20 years  nogin   I moved the bind operator from ITT to the Perv module. This makes sense because …
itt_srec.ml  3318  20 years  kopylov   - Fixed some bugs in Itt_w: (a) The rule ruduce_tree_eta was unsound (we could…
itt_srec.mli  2674  22 years  nogin   I removed @ from the parameter syntax for meta-parameters. Now [xxx:s] is parsed…
itt_struct.ml  3525  19 years  nogin   Minor ITT clean-up: - No need to use addHiddenLabelT when annotation on a rule w…
itt_struct.mli  3345  20 years  nogin   - Added a new tactic copyHypT for copying hypotheses (useful in elimination rule…
itt_struct.prla  3316  20 years  nogin   - Added "'H; x: 'A; 'J['x] >- "type"{'A}" to autoT - Fixed a few itt_fset proofs…
itt_struct2.ml  3312  20 years  kopylov   - Now substitution (s1=s2 in S) for conclution (t in T[s1]) produces a wf subgoa…
itt_struct2.mli  3257  20 years  kopylov   1. I added new primitive rules: Itt_struct.exchange Itt_pointwise.hypS…
itt_struct2.prla  3323  20 years  kopylov   Fix some proofs
itt_struct3.ml  3307  20 years  kopylov   - added rules applyEquality to intro resource - many rules (e.g. letT and elimi…
itt_struct3.mli  3307  20 years  kopylov   - added rules applyEquality to intro resource - many rules (e.g. letT and elimi…
itt_struct3.prla  3307  20 years  kopylov   - added rules applyEquality to intro resource - many rules (e.g. letT and elimi…
itt_subtype.ml  3348  20 years  kopylov   I changed the rule subtypeElimination2 and proved use_subtype1. Now elimination …
itt_subtype.mli  3348  20 years  kopylov   I changed the rule subtypeElimination2 and proved use_subtype1. Now elimination …
itt_subtype.prla  3348  20 years  kopylov   I changed the rule subtypeElimination2 and proved use_subtype1. Now elimination …
itt_test.ml  3329  20 years  nogin   I've removed old Itt_int* theories and switched all the ITT to Yegor's new theor…
itt_test.mli  2743  22 years  jyh   This is a major release; I bumped the release number to 0.6. WARNING: There are …
itt_theory.ml  3584  19 years  nogin   - Added the comment module to the theories.pdf ("make latex"). - Added a hack a…
itt_theory.mli  3329  20 years  nogin   I've removed old Itt_int* theories and switched all the ITT to Yegor's new theor…
itt_tsquash.ml  3319  20 years  kopylov   - Changed intro rule for the set type according to Alexey's beter_itt. - Proved…
itt_tsquash.mli  3298  20 years  kopylov   - All rules in record theories are prooved (except some simple arith facts). - …
itt_tsquash.prla  3298  20 years  kopylov   - All rules in record theories are prooved (except some simple arith facts). - …
itt_tunion.ml  3307  20 years  kopylov   - added rules applyEquality to intro resource - many rules (e.g. letT and elimi…
itt_tunion.mli  3047  20 years  nogin   I changed the unhide rules according to hide{A} = squash{A} semantics. Alexei, …
itt_tunion.prla  3307  20 years  kopylov   - added rules applyEquality to intro resource - many rules (e.g. letT and elimi…
itt_union.ml  3525  19 years  nogin   Minor ITT clean-up: - No need to use addHiddenLabelT when annotation on a rule w…
itt_union.mli  3223  20 years  nogin   Finally, I am able to commit what I was getting to in all these commits over the…
itt_union.prla  3300  20 years  kopylov   - I moved the rule quotientElimination2 to the Itt_pointwise2, since it is vali…
itt_unit.ml  3281  20 years  nogin   The redundant "_resource" suffix should not be used in resource names.
itt_unit.mli  3238  20 years  nogin   I rewrote the Itt_squash tactics and the squash_resource implementation and made…
itt_unit.prla  3232  20 years  nogin   I joined Itt_hide and Itt_squash into a single theory - Itt_squash that deals wi…
itt_void.ml  3292  20 years  nogin   *** IMPORTANT: before doing "cvs update" see warning below *** This commit impl…
itt_void.mli  3238  20 years  nogin   I rewrote the Itt_squash tactics and the squash_resource implementation and made…
itt_void.prla  3315  20 years  nogin   I have changed the way autoT works. Now autoT and trivialT share the same auto_…
itt_w.ml  3323  20 years  kopylov   Fix some proofs
itt_w.mli  3318  20 years  kopylov   - Fixed some bugs in Itt_w: (a) The rule ruduce_tree_eta was unsound (we could…
itt_w.prla  3318  20 years  kopylov   - Fixed some bugs in Itt_w: (a) The rule ruduce_tree_eta was unsound (we could…
itt_well_founded.ml  3584  19 years  nogin   - Added the comment module to the theories.pdf ("make latex"). - Added a hack a…
itt_well_founded.mli  2775  22 years  jyh   Things seem to be working pretty smoothly now. This is mostly minor fixes. Sti…
itt_well_founded.prla  3058  20 years  jyh   Last commit failed partway through...
jprover_tests.ml  3072  20 years  nogin   Bob's "Agatha" puzzle.
jprover_tests.mli  3001  21 years  nogin   Fixed a nasty bug in Jprover (after chaising it with Stephan for couple of hours…

Properties

Name Value
svn:ignore .consign .nfs* *.cm* Makefile.dep *.p4* *.ppo *.run *.opt ocamlprof.dump gmon.out *.prlb

  ViewVC Help
Powered by ViewVC 1.1.26