aboutsummaryrefslogtreecommitdiff
path: root/src/Util/ListUtil.v
Commit message (Expand)AuthorAge
* Add constr_fail and constr_fail_withGravatar Jason Gross2019-03-31
* Fix issue with previous commitGravatar Jason Gross2019-03-08
* Add some eq list_rect lemmas to ListUtilGravatar Jason Gross2019-03-08
* Add some eq lemmas to ListUtilGravatar Jason Gross2019-03-07
* Add some Proper lemmas to ListUtilGravatar Jason Gross2019-03-07
* Add remove_duplicatesGravatar Jason Gross2019-01-24
* prove [eval_conditional_sub]Gravatar jadep2018-12-21
* Add Forall2_update_nthGravatar Jason Gross2018-12-06
* Remove ListUtil.List.repeatGravatar Jason Gross2018-12-04
* Add map_repeat, map_constGravatar Jason Gross2018-11-11
* Add some natutil and listutil lemmasGravatar Jason Gross2018-10-10
* Add map_update_nth_extGravatar Jason Gross2018-10-09
* Add some util lemmasGravatar Jason Gross2018-08-13
* Add ListUtil.map_nth_default_seqGravatar Jason Gross2018-08-10
* Add ListUtil.{combine_repeat,combine_rev_rev_samelength}Gravatar Jason Gross2018-08-09
* Add nth_error_combineGravatar Jason Gross2018-08-01
* Add more proper instancesGravatar Jason Gross2018-07-26
* Add ListUtil.{take,drop}_whileGravatar Jason Gross2018-07-24
* Add minor lemmas to utilGravatar Jason Gross2018-07-17
* Add ZUtil, list lemmasGravatar Jason Gross2018-07-02
* Fix a notation issue in previous commitGravatar Jason Gross2018-07-02
* Add more ListUtil proofsGravatar Jason Gross2018-07-02
* Add some list lemmasGravatar Jason Gross2018-07-02
* Add useful list lemmasGravatar Jason Gross2018-06-29
* Add list_beqGravatar Jason Gross2018-06-22
* Add seq_add, seq_len_0Gravatar Jason Gross2018-06-19
* Move function argument out of fixpoint of List.map2Gravatar Jason Gross2018-05-21
* add a list lemmaGravatar Jade Philipoom2018-04-11
* pass-through after Andres's review in #334Gravatar Jade Philipoom2018-04-03
* move some lemmas to ZUtil/ListUtilGravatar Jade Philipoom2018-04-03
* move some lemmas/hints to ListUtilGravatar Jade Philipoom2018-04-03
* Add list_case, a definition for match on listGravatar Jason Gross2018-03-27
* add two proofs about listsGravatar Jade Philipoom2018-02-23
* Strip the pointed instance names off of the default value in list expansionGravatar Jason Gross2018-02-18
* Add expand_lists tacticGravatar Jason Gross2018-02-18
* Add expand_list_correct to ListUtilGravatar Jason Gross2018-02-12
* Generalize Forall2_forall_iffGravatar Jason Gross2017-11-09
* src/Demo.v: a 200-line introduction to BaseSystem ideasGravatar Andres Erbsen2017-06-21
* Don't rely on autogenerated namesGravatar Jason Gross2017-06-05
* s/appcontext/context/Gravatar Jason Gross2017-05-11
* do not use VerdiTactics in files we plan to keepGravatar Andres Erbsen2017-04-06
* Add [Proof using] to most proofsGravatar Jason Gross2017-04-04
* Add lemmas needed for saturated arithmetic [compact]Gravatar jadep2017-03-24
* Add {firstn,skipn}_seqGravatar Jason Gross2017-03-19
* generalize In_firstn_skipn_splitGravatar Jason Gross2017-03-19
* Add In_firstn_skipn_splitGravatar Jason Gross2017-03-19
* Add firstn_firstn_minGravatar Jason Gross2017-03-19
* Fix a name clashGravatar Jason Gross2017-03-14
* Add firstn_skipnGravatar Jason Gross2017-03-14
* Add skipn_skipnGravatar Jason Gross2017-03-14
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-29 19:06:51 +0000