aboutsummaryrefslogtreecommitdiff
path: root/src/Util/ListUtil.v
Commit message (Expand)AuthorAge
* 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
* added Positional wrappers for Associational operations, added correctness pro...Gravatar jadep2017-02-27
* prove admits in Util.TupleGravatar Andres Erbsen2016-11-11
* Add fold_right_andb_true_iff_fold_right_and_TrueGravatar Jason Gross2016-10-19
* Add Tuple.map2Gravatar Jason Gross2016-10-19
* Work around bug #5112 ([Arguments id /] broken)Gravatar Jason Gross2016-09-30
* Move side lemmas to appropriate filesGravatar jadep2016-09-17
* Add nth_error_In from 8.6Gravatar Jason Gross2016-09-05
* Added rewrite hints for two ListUtil lemmasGravatar jadep2016-08-24
* Fix a typoGravatar Jason Gross2016-08-24
* Add map_cons from Coq 8.6Gravatar Jason Gross2016-08-24
* ListUtil.v : new proofs about sum_firstn for lists with nonnegative elementsGravatar jadep2016-08-21
* More 8.4 compatGravatar Jason Gross2016-08-16
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-11 16:05:16 +0000