index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
Reflection
/
WfProofs.v
Commit message (
Expand
)
Author
Age
*
Adjust implicits of flatten_binding_list_same_in_eq
Jason Gross
2017-03-01
*
Add flatten_binding_list_In_eq_iff, flatten_binding_list_same_in_eq
Jason Gross
2017-03-01
*
Switch to fully uncurried form for reflection
Jason Gross
2017-03-01
*
Prove nicer version of wf_SmartAbs
Jason Gross
2017-02-13
*
Add partially admitted lemma wf_SmartAbs
Jason Gross
2017-02-13
*
Add wf database
Jason Gross
2017-02-01
*
Add wff_SmartVarVarf_nil
Jason Gross
2017-02-01
*
Add In_G_wff_SmartVarf, SmartVarf_Pair
Jason Gross
2017-01-30
*
Split off some bits of Reflection.Syntax
Jason Gross
2017-01-26
*
Add flatten_binding_list2_SmartVarfMap{1,2}
Jason Gross
2017-01-25
*
Lemmas about flatten_binding_list2
Jason Gross
2017-01-25
*
Generalize flatten_binding_list_SmartValf
Jason Gross
2017-01-24
*
Add flatten_binding_list_SmartValf
Jason Gross
2017-01-24
*
Add flatten_binding_list_SmartVarfMap
Jason Gross
2017-01-24
*
Remove the Const constructor of exprf
Jason Gross
2017-01-19
*
Move things to ExprInversion
Jason Gross
2016-12-03
*
Add [f] to things that use [exprf] or [flat_type]
Jason Gross
2016-10-31
*
Add more WfProofs
Jason Gross
2016-10-29
*
Add interp_type_gen_rel_pointwise2, *_gen => *
Jason Gross
2016-10-28
*
Split off lemmas about [InlineConst]
Jason Gross
2016-09-16
*
Reorder WfProofs arguments
Jason Gross
2016-09-05
*
Fix order of binders, and add WfProofs
Jason Gross
2016-09-05