index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
Experiments
/
NewPipeline
/
LanguageWf.v
Commit message (
Expand
)
Author
Age
*
Add wf_from_flat_to_flat
Jason Gross
2018-09-12
*
Revert "Revert "Add more instances for type.related""
Jason Gross
2018-08-20
*
Revert "Add more instances for type.related"
Jason Gross
2018-08-17
*
Be more judicious about an instance
Jason Gross
2018-08-17
*
Add and_eqv_for_each_lhs_of_arrow_not_higher_order
Jason Gross
2018-08-16
*
Add more instances for type.related
Jason Gross
2018-08-16
*
Add related_hetero_iff_app_curried
Jason Gross
2018-08-10
*
Add more interp lemmas
Jason Gross
2018-08-09
*
Add Wf_of_Wf3
Jason Gross
2018-08-08
*
Add lemmas about type.and_for_each_lhs_of_arrow
Jason Gross
2018-08-07
*
Add another GeneralizeVar pass to add support for using Wf3
Jason Gross
2018-08-07
*
Add gen_interp_Proper
Jason Gross
2018-08-06
*
Add app_curried_Proper_gen as an instance
Jason Gross
2018-08-06
*
Add related_iff_app_curried
Jason Gross
2018-08-06
*
Generalize interp flat lemmas
Jason Gross
2018-08-06
*
Generalize wf_interp_Proper
Jason Gross
2018-08-06
*
Add wf for DefaultValue
Jason Gross
2018-08-03
*
Make wf_safe_t a bit stronger
Jason Gross
2018-08-02
*
Generalize type.eqv a bit
Jason Gross
2018-07-30
*
Integrate Wf and Interp proofs
Jason Gross
2018-07-30
*
More proofs about wf / interp
Jason Gross
2018-07-27
*
Add wf about reify/reflect list
Jason Gross
2018-07-27
*
Move rewrites to the correct tactic
Jason Gross
2018-07-26
*
Shuffle transport lemmas around, add more inversion
Jason Gross
2018-07-26
*
Improve wf tactics
Jason Gross
2018-07-26
*
Minor improvements to wf framework
Jason Gross
2018-07-26
*
Move some tactics to their proper place
Jason Gross
2018-07-26
*
Add Wf lemmas about SubstVar
Jason Gross
2018-07-26
*
Add basic wf proofs
Jason Gross
2018-07-26