| Commit message (Expand) | Author | Age |
* | 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 |
* | change map_with to mapi_with, a version that handles the index explicitly | jadep | 2017-03-29 |
* | More robust reifier | Jason Gross | 2017-03-29 |
* | Add Z.one_succ Z.two_succ to zsimplify_const db | Jason Gross | 2017-03-28 |
* | Don't reserve '(max_bitwidth' | Jason Gross | 2017-03-28 |
* | Add a notation for printing | Jason Gross | 2017-03-28 |
* | Add Z.FoldTypes.{Min,Max}TypeUsed | Jason Gross | 2017-03-28 |
* | Add FoldTypes | Jason Gross | 2017-03-28 |
* | Add Wf_MapCast_arrow | Jason Gross | 2017-03-28 |
* | Add InterpExprEta_arrow | Jason Gross | 2017-03-28 |
* | Add Wf_MapCast to wf database | Jason Gross | 2017-03-28 |
* | Break up MapCast into separate pieces for easier debugging | Jason Gross | 2017-03-28 |
* | make update-_CoqProject | Jason Gross | 2017-03-28 |
* | Finish proof of wf_map_cast | Jason Gross | 2017-03-28 |
* | Do more subst in ContextProperties/Tactics | Jason Gross | 2017-03-28 |
* | Add find_Name_and_val_SmartFlatTypeMapUnInterp2_Some_Some | Jason Gross | 2017-03-28 |
* | Add SmartVarfMap3 arguments | Jason Gross | 2017-03-28 |
* | Add SmartVarfMap3 | Jason Gross | 2017-03-28 |
* | Add Bounds.dec_eq_interp_flat_type | Jason Gross | 2017-03-27 |
* | crypto-defects.md: add two tweetnacl bugs | Andres Erbsen | 2017-03-26 |
* | Added saturated arithmetic file, including [compact] code and proof | jadep | 2017-03-24 |
* | Add lemmas needed for saturated arithmetic [compact] | jadep | 2017-03-24 |
* | Fix binder counting in MapCastByDB | Jason Gross | 2017-03-22 |
* | Add aborted CompileProperties | Jason Gross | 2017-03-22 |
* | Add split_onames_split_names | Jason Gross | 2017-03-22 |
* | Add length_fst_split_names_None_iff | Jason Gross | 2017-03-22 |
* | Also count lets in operations and pairs | Jason Gross | 2017-03-22 |