| 2011-01-19 |
Wilmer Ricciotti | Added some typing info to elimination principles, allowing...
|
commit | commitdiff | tree |
| 2010-12-22 |
Wilmer Ricciotti | more theory for lists
|
commit | commitdiff | tree |
| 2010-12-22 |
Wilmer Ricciotti | ...
|
commit | commitdiff | tree |
| 2010-07-28 |
Wilmer Ricciotti | Fixes unexpected behaviour of ncut when multiple goals...
|
commit | commitdiff | tree |
| 2010-07-28 |
Wilmer Ricciotti | Experimental enhancements to the ndestruct tactic....
|
commit | commitdiff | tree |
| 2010-06-10 |
Wilmer Ricciotti | Fix for inversion principles of types with a single...
|
commit | commitdiff | tree |
| 2010-06-08 |
Wilmer Ricciotti | Fixed a bug in the undebruijnate function which caused...
|
commit | commitdiff | tree |
| 2010-05-12 |
Wilmer Ricciotti | Library support files for John Major equality and Russell.
|
commit | commitdiff | tree |
| 2010-05-12 |
Wilmer Ricciotti | Experimental support for Russell (coercions moving...
|
commit | commitdiff | tree |
| 2010-05-06 |
Wilmer Ricciotti | Fixing naming scheme for composite coercions.
|
commit | commitdiff | tree |
| 2010-05-04 |
Wilmer Ricciotti | * Fixed a couple of glitches in ndestruct
|
commit | commitdiff | tree |
| 2010-03-31 |
Wilmer Ricciotti | Added test file for inversion in ng matita.
|
commit | commitdiff | tree |
| 2010-03-25 |
Wilmer Ricciotti | Z.ma updated to reflect changes in the logical Not...
|
commit | commitdiff | tree |
| 2010-03-02 |
Wilmer Ricciotti | Added reverse rewriting principle in Type[0].
|
commit | commitdiff | tree |
| 2010-03-02 |
Wilmer Ricciotti | Some integrations to the ng library.
|
commit | commitdiff | tree |
| 2010-03-02 |
Wilmer Ricciotti | Added syntax for ninversion tactic (still experimental).
|
commit | commitdiff | tree |
| 2010-03-01 |
Wilmer Ricciotti | Fixed a bug in the unification, which prevented some...
|
commit | commitdiff | tree |
| 2010-02-25 |
Wilmer Ricciotti | Minimal example in Z showing a problem in the nnormalize...
|
commit | commitdiff | tree |
| 2010-02-03 |
Wilmer Ricciotti | Disabled debug prints in ndestruct tactic.
|
commit | commitdiff | tree |
| 2010-02-02 |
Wilmer Ricciotti | New version using Streicher's K axiom. Should be faster...
|
commit | commitdiff | tree |
| 2010-02-02 |
Wilmer Ricciotti | Added Streicher's K axiom.
|
commit | commitdiff | tree |
| 2010-02-02 |
Wilmer Ricciotti | Fixed a bug with indexed inductive types which sometimes...
|
commit | commitdiff | tree |
| 2010-01-12 |
Wilmer Ricciotti | Fixed a bug in the discrimination principle: the refiner...
|
commit | commitdiff | tree |
| 2009-12-04 |
Wilmer Ricciotti | Bugfix in inversion (was using refl_eq instead of refl).
|
commit | commitdiff | tree |
| 2009-11-27 |
Wilmer Ricciotti | ndestruct now clears off identity equations whenever...
|
commit | commitdiff | tree |
| 2009-11-25 |
Wilmer Ricciotti | Fixed inversion, which was broken by the last changes...
|
commit | commitdiff | tree |
| 2009-11-24 |
Wilmer Ricciotti | Bugfix in tipify: a metavariable was set to type without...
|
commit | commitdiff | tree |
| 2009-11-24 |
Wilmer Ricciotti | In order to prevent useless meta extensions, we optimize...
|
commit | commitdiff | tree |
| 2009-11-24 |
Wilmer Ricciotti | When unifying
|
commit | commitdiff | tree |
| 2009-11-19 |
Wilmer Ricciotti | - Added a swap parameter to the unification procedure
|
commit | commitdiff | tree |
| 2009-11-18 |
Wilmer Ricciotti | NCicRefiner.force_to_sort implemented on top of NCicUnificat...
|
commit | commitdiff | tree |
| 2009-11-18 |
Wilmer Ricciotti | Code factorization for check_type.
|
commit | commitdiff | tree |
| 2009-11-17 |
Wilmer Ricciotti | ndestruct tactic: mainly bugfixes; the algorithm isn...
|
commit | commitdiff | tree |
| 2009-11-16 |
Wilmer Ricciotti | Implementation of ndestruct tactic (including destruction...
|
commit | commitdiff | tree |
| 2009-10-20 |
Wilmer Ricciotti | ...
|
commit | commitdiff | tree |
| 2009-10-13 |
Wilmer Ricciotti | Experimental scripts for nth-order rewriting principles.
|
commit | commitdiff | tree |
| 2009-10-06 |
Wilmer Ricciotti | Syntax highlighting for 'ninverter' keyword
|
commit | commitdiff | tree |
| 2009-10-06 |
Wilmer Ricciotti | Inverters/Inversion:
|
commit | commitdiff | tree |
| 2009-10-02 |
Wilmer Ricciotti | Updated command ninverter. Syntax:
|
commit | commitdiff | tree |
| 2009-09-30 |
Wilmer Ricciotti | Added initial support for inversion principles in Matita NG.
|
commit | commitdiff | tree |
| 2009-07-20 |
Wilmer Ricciotti | Final version, submitted to CASC-22.
|
commit | commitdiff | tree |
| 2009-07-20 |
Wilmer Ricciotti | added a flag for age selection
|
commit | commitdiff | tree |
| 2009-07-15 |
Wilmer Ricciotti | Fixed dependency function, which was lacking the code...
|
commit | commitdiff | tree |
| 2009-07-09 |
Wilmer Ricciotti | More updates to Fsub.
|
commit | commitdiff | tree |
| 2009-07-01 |
Wilmer Ricciotti | Version number set to 1.0.0-rc1
|
commit | commitdiff | tree |
| 2009-06-21 |
Wilmer Ricciotti | Added injective compose
|
commit | commitdiff | tree |
| 2009-06-20 |
Wilmer Ricciotti | Some notation and additional lemmata.
|
commit | commitdiff | tree |
| 2009-06-19 |
Wilmer Ricciotti | More improvements.
|
commit | commitdiff | tree |
| 2009-06-05 |
Wilmer Ricciotti | - replaced part1a/defn with the version based on induction...
|
commit | commitdiff | tree |
| 2009-06-03 |
Wilmer Ricciotti | Update, using induction/inversion.
|
commit | commitdiff | tree |
| 2009-05-29 |
Wilmer Ricciotti | POPLmark part 1a using the de Bruijn encoding.
|
commit | commitdiff | tree |
| 2009-04-22 |
Wilmer Ricciotti | syntax colouring for inverters
|
commit | commitdiff | tree |
| 2009-04-22 |
Wilmer Ricciotti | Disabled debug prints in the inversion principle.
|
commit | commitdiff | tree |
| 2009-04-22 |
Wilmer Ricciotti | New command "inverter" used to generate an induction...
|
commit | commitdiff | tree |
| 2009-02-13 |
Wilmer Ricciotti | Axiomatization of real numbers (work in progress)
|
commit | commitdiff | tree |
| 2008-12-15 |
Wilmer Ricciotti | Some changes to the pullback test, for debugging
|
commit | commitdiff | tree |
| 2008-12-15 |
Wilmer Ricciotti | First attempt to implement unification hints.
|
commit | commitdiff | tree |
| 2008-10-08 |
Wilmer Ricciotti | Fixed a performance problem with unif_machines and...
|
commit | commitdiff | tree |
| 2008-10-03 |
Wilmer Ricciotti | Final implementation of proof irrelevant conversion...
|
commit | commitdiff | tree |
| 2008-08-12 |
Wilmer Ricciotti | Fixed two legacy comments
|
commit | commitdiff | tree |
| 2008-07-02 |
Wilmer Ricciotti | Fixed a bug which prevented mutually recursive definitions...
|
commit | commitdiff | tree |
| 2008-06-13 |
Wilmer Ricciotti | final relevance check
|
commit | commitdiff | tree |
| 2008-06-10 |
Wilmer Ricciotti | relevance check for Match
|
commit | commitdiff | tree |
| 2008-06-10 |
Wilmer Ricciotti | Added check of relevance lists for inductive types...
|
commit | commitdiff | tree |
| 2008-06-09 |
Wilmer Ricciotti | Reverting to the previous version some files which...
|
commit | commitdiff | tree |
| 2008-06-09 |
Wilmer Ricciotti | more proof irrelevance
|
commit | commitdiff | tree |
| 2008-06-04 |
Wilmer Ricciotti | Proof-irrelevance check for all applications (first...
|
commit | commitdiff | tree |
| 2008-06-04 |
Wilmer Ricciotti | incomplete irrelevance test commented out
|
commit | commitdiff | tree |
| 2008-05-02 |
Wilmer Ricciotti | Some destruct tactics got broken after last update...
|
commit | commitdiff | tree |
| 2008-04-24 |
Wilmer Ricciotti | Proof of adequacy.
|
commit | commitdiff | tree |
| 2008-03-27 |
Wilmer Ricciotti | Updated depedencies.
|
commit | commitdiff | tree |
| 2008-03-26 |
Wilmer Ricciotti | Reorganization of list library (step 1)
|
commit | commitdiff | tree |
| 2008-03-25 |
Wilmer Ricciotti | small update
|
commit | commitdiff | tree |
| 2008-02-27 |
Wilmer Ricciotti | the proof of bertrand's conjecture is now complete
|
commit | commitdiff | tree |
| 2008-02-22 |
Wilmer Ricciotti | sieve of erathostene (proof of soundness almost done)
|
commit | commitdiff | tree |
| 2008-02-05 |
Wilmer Ricciotti | lower bound for neper's constant
|
commit | commitdiff | tree |
| 2008-01-31 |
Wilmer Ricciotti | One Obj.magic implemented, trust changed to false.
|
commit | commitdiff | tree |
| 2008-01-31 |
Wilmer Ricciotti | Transformation back and forth between old and new representation
|
commit | commitdiff | tree |
| 2008-01-31 |
Wilmer Ricciotti | Square root added.
|
commit | commitdiff | tree |
| 2008-01-22 |
Wilmer Ricciotti | Bertrand's conjecture (weak), some work in progress
|
commit | commitdiff | tree |
| 2008-01-15 |
Wilmer Ricciotti | update: upper bound for prim
|
commit | commitdiff | tree |
| 2008-01-14 |
Wilmer Ricciotti | Chebyshev's upper bound on prim
|
commit | commitdiff | tree |
| 2007-12-21 |
Wilmer Ricciotti | beginning proof of chebyshev's bound on prim.
|
commit | commitdiff | tree |
| 2007-12-17 |
Wilmer Ricciotti | upper bound for logarithmic summation
|
commit | commitdiff | tree |
| 2007-12-12 |
Wilmer Ricciotti | Progress.
|
commit | commitdiff | tree |
| 2007-12-09 |
Wilmer Ricciotti | Added summation formula for the power of a binomial.
|
commit | commitdiff | tree |
| 2007-10-12 |
Wilmer Ricciotti | Fixed baseuri
|
commit | commitdiff | tree |
| 2007-10-12 |
Wilmer Ricciotti | Part1a update...
|
commit | commitdiff | tree |
| 2007-09-24 |
Wilmer Ricciotti | Last version of poplmark 1a, featuring new proof, only...
|
commit | commitdiff | tree |
| 2007-09-12 |
Wilmer Ricciotti | Updated, proofs are now about 750 lines.
|
commit | commitdiff | tree |
| 2007-07-26 |
Wilmer Ricciotti | Some notation added
|
commit | commitdiff | tree |
| 2007-07-16 |
Wilmer Ricciotti | corrected axiom mod_plus
|
commit | commitdiff | tree |
| 2007-06-21 |
Wilmer Ricciotti | PoplMark challenge part 1a: new, shorter version w...
|
commit | commitdiff | tree |
| 2007-01-18 |
Wilmer Ricciotti | new version, using new tacticals
|
commit | commitdiff | tree |
| 2006-11-30 |
Wilmer Ricciotti | library/Fsub: minor fix
|
commit | commitdiff | tree |
| 2006-11-30 |
Wilmer Ricciotti | library: added solution to POPLMark challenge part...
|
commit | commitdiff | tree |
|
projects / helm.git / search