aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
...
* Rewrite in Op arguments before rewriting in OpGravatar Jason Gross2017-04-01
* Also do eta under lets in Reflection/Eta.vGravatar Jason Gross2017-04-01
* Add an initial glue file in the pipeline, no option in boundsGravatar Jason Gross2017-04-01
* Fix definition of BoundedWordGravatar Jason Gross2017-04-01
* Split off BoundedWord.v from IntegrationTest.vGravatar Jason Gross2017-04-01
* Add back word hex constant notationsGravatar Jason Gross2017-04-01
* Add RenameBindersGravatar Jason Gross2017-04-01
* Add wf proof for arithmetic simpliferGravatar Jason Gross2017-04-01
* Fix a name (sprurious interp)Gravatar Jason Gross2017-04-01
* Add interp proof for arithmetic simplifierGravatar Jason Gross2017-04-01
* Handle inversion of homogenous products in reflective type inversionGravatar Jason Gross2017-04-01
* Add an arithmetic simplifierGravatar Jason Gross2017-04-01
* Add correctness of RewriterGravatar Jason Gross2017-04-01
* Add Reflection/Rewriter.vGravatar Jason Gross2017-04-01
* Split out Tactics.SubstLetGravatar Jason Gross2017-04-01
* Remove trailing whitespace in NewBaseSystemGravatar Jason Gross2017-04-01
* Add Tuple.etaGravatar Jason Gross2017-04-01
* insert a reduce step in the correct place of the carry chainGravatar jadep2017-04-01
* Alter relax_output_bounds statementGravatar Jason Gross2017-04-01
* Add a bounds relaxation lemmaGravatar Jason Gross2017-03-31
* Add Z.log2_up_le_pow2_fullGravatar Jason Gross2017-03-31
* Fix inversion_base_typeGravatar Jason Gross2017-03-31
* Add inversion_base_type for Z.Syntax.base_typeGravatar Jason Gross2017-03-31
* Add Bounds.is_tighter_thanbGravatar Jason Gross2017-03-31
* Use a better order of arguments for Bounds.is_bounded_byGravatar Jason Gross2017-03-31
* Add is_tighter_than_bool to zrangeGravatar Jason Gross2017-03-31
* More compatibility for etransitivityGravatar Jason Gross2017-03-31
* Add [change_with_curried] to Curry.vGravatar Jason Gross2017-03-31
* Add [etransitivity y], [etransitivity_rev] tacticsGravatar Jason Gross2017-03-31
* use improved fsatz on various elliptic curve thingsGravatar Andres Erbsen2017-03-31
* Add a comment explaining bounds_expGravatar Jason Gross2017-03-30
* Add wordToZ{_gen,}_rangeGravatar Jason Gross2017-03-30
* Update IntegrationTest with actual boundsGravatar Jason Gross2017-03-30
* Start instantiating MapCastByDeBruijn in Z/Gravatar Jason Gross2017-03-30
* Created test file for newbasesystem/word-size-selection integrationGravatar jadep2017-03-30
* turn [Let]s into [Definition]s so they persist after the sectionGravatar jadep2017-03-30
* Reorder arguments to Wf_MapCast for eautoGravatar Jason Gross2017-03-30
* fix a typoGravatar jadep2017-03-30
* change import order to avoid name-clash with [List.repeat] and [Tuple.repeat]Gravatar jadep2017-03-30
* Don't linearize and eta in MapCastByDeBruijnGravatar Jason Gross2017-03-30
* Revert "Update CNotations, JavaNotations"Gravatar Jason Gross2017-03-30
* rename [Sorted] to [Columns]Gravatar jadep2017-03-30
* Proofs for [Sorted.from_associational]Gravatar jadep2017-03-30
* create module, indent the things, also rewrite [nils] to use tuple [repeat] a...Gravatar jadep2017-03-30
* rewrite zeros to use tuple [repeat]Gravatar jadep2017-03-30
* added tuple [repeat]Gravatar jadep2017-03-30
* Update CNotations, JavaNotationsGravatar Jason Gross2017-03-30
* Use r[_ ~> _] for range rather than b[_ ~> _]Gravatar Jason Gross2017-03-30
* Rename Bounds to ZRange, use Prop, not boolGravatar Jason Gross2017-03-30
* Get rid of list-based Tuple.mapGravatar Jason Gross2017-03-30
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 06:47:54 +0000