index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
Util
/
Tuple.v
Commit message (
Expand
)
Author
Age
*
write and prove Tuple.map2_cps
jadep
2017-06-25
*
Add is_bounded_by_None_repeat_In_iff
Jason Gross
2017-06-20
*
Don't rely on autogenerated names
Jason Gross
2017-06-05
*
prove compact obeys div/mod rule
jadep
2017-05-01
*
added [lastn] for tuples
jadep
2017-05-01
*
Fix nth_default for the tip of v8.6
Jason Gross
2017-04-28
*
add nth_default on tuple
jadep
2017-04-28
*
Add [Proof using] to most proofs
Jason Gross
2017-04-04
*
Add Tuple.map_Proper
Jason Gross
2017-04-03
*
Coalesce Tuple.pointwise2 and Tuple.fieldwise
Jason Gross
2017-04-02
*
Add Tuple.eta
Jason Gross
2017-04-01
*
added tuple [repeat]
jadep
2017-03-30
*
Get rid of list-based Tuple.map
Jason Gross
2017-03-30
*
Add Tuple.pointwise2, Tuple.map_fix
Jason Gross
2017-03-30
*
change map_with to mapi_with, a version that handles the index explicitly
jadep
2017-03-29
*
Add lemmas needed for saturated arithmetic [compact]
jadep
2017-03-24
*
Add strip_eta_tuple lemmas
Jason Gross
2017-02-28
*
Better tuple_eta arguments
Jason Gross
2017-02-28
*
Add eta_tuple functions
Jason Gross
2017-02-28
*
More fine-grained util tactic files
Jason Gross
2017-01-17
*
More universe fixes
Jason Gross
2017-01-15
*
Fix an issue with universes
Jason Gross
2017-01-15
*
Add tuple lemmas
Jason Gross
2016-11-22
*
Add fieldwise_map
Jason Gross
2016-11-17
*
use @implicits in rewrite (8.4)
Andres Erbsen
2016-11-11
*
prove admits in Util.Tuple
Andres Erbsen
2016-11-11
*
Add Tuple and HList lemmas
Jason Gross
2016-11-10
*
Fix bug in 8.4
Jason Gross
2016-11-09
*
Add assoc_right
Jason Gross
2016-11-09
*
Fix Tuple.map2_S
Jason Gross
2016-11-09
*
Add Tuple.map2_S
Jason Gross
2016-11-08
*
Add map2_map{,_fst,_snd}
Jason Gross
2016-11-08
*
Rename iffT, add some lemmas about tuple and hlist
Jason Gross
2016-11-08
*
Work around bug in 8.4
Jason Gross
2016-11-08
*
Add push_lift_option
Jason Gross
2016-11-07
*
Add tuple hd and tl
Jason Gross
2016-11-07
*
Add more admitted tuple lemmas
Jason Gross
2016-11-06
*
Add more admitted tuple lemmas
Jason Gross
2016-11-06
*
Add Tuple.map_map2 (admitted)
Jason Gross
2016-11-06
*
Add admitted lemma about tuple map, add hlist lem
Jason Gross
2016-11-06
*
Add Tuple lift push
Jason Gross
2016-11-06
*
Add functions for [tuple (option _) _]
Jason Gross
2016-11-06
*
Move hlist to new file
Jason Gross
2016-11-01
*
Fix a typo in the previous commit
Jason Gross
2016-11-01
*
Generalize hlist
Jason Gross
2016-11-01
*
Add hlist to tuple
Jason Gross
2016-11-01
*
Fix implicit status of curry
Jason Gross
2016-10-27
*
Add curry and uncurry to tuple
Jason Gross
2016-10-27
*
Fix for Coq 8.4
Jason Gross
2016-10-24
*
Add more relations about fieldwise
Jason Gross
2016-10-24
[next]