| Commit message (Expand) | Author | Age |
... | |
* | Add wf proof for arithmetic simplifer | Jason Gross | 2017-04-01 |
* | Fix a name (sprurious interp) | Jason Gross | 2017-04-01 |
* | Add interp proof for arithmetic simplifier | Jason Gross | 2017-04-01 |
* | Handle inversion of homogenous products in reflective type inversion | Jason Gross | 2017-04-01 |
* | Add an arithmetic simplifier | Jason Gross | 2017-04-01 |
* | Add correctness of Rewriter | Jason Gross | 2017-04-01 |
* | Add Reflection/Rewriter.v | Jason Gross | 2017-04-01 |
* | Split out Tactics.SubstLet | Jason Gross | 2017-04-01 |
* | Remove trailing whitespace in NewBaseSystem | Jason Gross | 2017-04-01 |
* | Add Tuple.eta | Jason Gross | 2017-04-01 |
* | insert a reduce step in the correct place of the carry chain | jadep | 2017-04-01 |
* | Alter relax_output_bounds statement | Jason Gross | 2017-04-01 |
* | Add a bounds relaxation lemma | Jason Gross | 2017-03-31 |
* | Add Z.log2_up_le_pow2_full | Jason Gross | 2017-03-31 |
* | Fix inversion_base_type | Jason Gross | 2017-03-31 |
* | Add inversion_base_type for Z.Syntax.base_type | Jason Gross | 2017-03-31 |
* | Add Bounds.is_tighter_thanb | Jason Gross | 2017-03-31 |
* | Use a better order of arguments for Bounds.is_bounded_by | Jason Gross | 2017-03-31 |
* | Add is_tighter_than_bool to zrange | Jason Gross | 2017-03-31 |
* | More compatibility for etransitivity | Jason Gross | 2017-03-31 |
* | Add [change_with_curried] to Curry.v | Jason Gross | 2017-03-31 |
* | Add [etransitivity y], [etransitivity_rev] tactics | Jason Gross | 2017-03-31 |
* | use improved fsatz on various elliptic curve things | Andres Erbsen | 2017-03-31 |
* | Add a comment explaining bounds_exp | Jason Gross | 2017-03-30 |
* | Add wordToZ{_gen,}_range | Jason Gross | 2017-03-30 |
* | Update IntegrationTest with actual bounds | Jason Gross | 2017-03-30 |
* | Start instantiating MapCastByDeBruijn in Z/ | Jason Gross | 2017-03-30 |
* | Created test file for newbasesystem/word-size-selection integration | jadep | 2017-03-30 |
* | turn [Let]s into [Definition]s so they persist after the section | jadep | 2017-03-30 |
* | Reorder arguments to Wf_MapCast for eauto | Jason Gross | 2017-03-30 |
* | fix a typo | jadep | 2017-03-30 |
* | change import order to avoid name-clash with [List.repeat] and [Tuple.repeat] | jadep | 2017-03-30 |
* | Don't linearize and eta in MapCastByDeBruijn | Jason Gross | 2017-03-30 |
* | Revert "Update CNotations, JavaNotations" | Jason Gross | 2017-03-30 |
* | rename [Sorted] to [Columns] | jadep | 2017-03-30 |
* | Proofs for [Sorted.from_associational] | jadep | 2017-03-30 |
* | create module, indent the things, also rewrite [nils] to use tuple [repeat] a... | jadep | 2017-03-30 |
* | rewrite zeros to use tuple [repeat] | jadep | 2017-03-30 |
* | added tuple [repeat] | jadep | 2017-03-30 |
* | Update CNotations, JavaNotations | Jason Gross | 2017-03-30 |
* | Use r[_ ~> _] for range rather than b[_ ~> _] | Jason Gross | 2017-03-30 |
* | Rename Bounds to ZRange, use Prop, not bool | Jason Gross | 2017-03-30 |
* | Get rid of list-based Tuple.map | Jason Gross | 2017-03-30 |
* | Use Bounds in BoundsInterpretations | Jason Gross | 2017-03-30 |
* | make fsatz recurse when proving nonzero-ness, undo Weierstrass workaround | Andres Erbsen | 2017-03-30 |
* | Add a file dedicated to the definition of Z bounds | Jason Gross | 2017-03-30 |
* | Add Tuple.pointwise2, Tuple.map_fix | Jason Gross | 2017-03-30 |
* | some examples/tests for compact | jadep | 2017-03-29 |
* | convert compact to CPS and try out a simple example | jadep | 2017-03-29 |
* | remove commented-out lemma and add CPS version of mapi_with | jadep | 2017-03-29 |