index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
Experiments
Commit message (
Expand
)
Author
Age
...
*
Add type.related_hetero
Jason Gross
2018-07-30
*
Allow proving force ∘ thunk = id extensionally
Jason Gross
2018-07-30
*
Add UnderLets.wf_Proper_list
Jason Gross
2018-07-30
*
Add wf_splice
Jason Gross
2018-07-30
*
Generalize type.eqv a bit
Jason Gross
2018-07-30
*
Some WIP on Rewiter correctness
Jason Gross
2018-07-30
*
Integrate Wf and Interp proofs
Jason Gross
2018-07-30
*
Add wf and interp proofs for LetBindReturn
Jason Gross
2018-07-27
*
More proofs about wf / interp
Jason Gross
2018-07-27
*
Add wf about reify/reflect list
Jason Gross
2018-07-27
*
Stronger inversion
Jason Gross
2018-07-27
*
Add invert_nil, invert_cons
Jason Gross
2018-07-27
*
Set arguments of ident.{gen_,}interp
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
*
Add Wf proofs about MiscCompilerPasses
Jason Gross
2018-07-26
*
Move the associator pass to the rewriter
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
*
Put == in type_scope, so that we don't need to go around opening etype_scope
Jason Gross
2018-07-26
*
Add basic wf proofs
Jason Gross
2018-07-26
*
Actually improve expr.invert_one
Jason Gross
2018-07-26
*
Try again to fix expr inversion
Jason Gross
2018-07-26
*
Improve expr.invert_one (hopefully)
Jason Gross
2018-07-26
*
Add type.eqv for interp equivalence
Jason Gross
2018-07-26
*
Add some inversion lemmas and tactics
Jason Gross
2018-07-25
*
Add invert_LetIn
Jason Gross
2018-07-25
*
Improve rewriter speed
Jason Gross
2018-07-25
*
Revert "Improve rewriter speed"
Jason Gross
2018-07-24
*
Improve rewriter speed
Jason Gross
2018-07-24
*
Montgomery reduction in new pipeline
Jason Gross
2018-07-21
*
Support reification of firstn, skipn
Jason Gross
2018-07-18
*
vm_compute in peel_interp_app
Jason Gross
2018-07-18
*
Thunk nat_rect for better perf, list_{rect=>case}
Jason Gross
2018-07-17
*
Remove a lemma that's been moved to NatUtil
Jason Gross
2018-07-17
*
Allow reification of nat_rect (fun _ => _ -> _)
Jason Gross
2018-07-15
*
Add a stronger version of eval_reduce
Jason Gross
2018-07-14
*
Partial adaptation to https://github.com/coq/coq/pull/8063
Jason Gross
2018-07-14
*
Better error message printing
Jason Gross
2018-07-12
*
Remove useless dependency
Jason Gross
2018-07-12
*
Make Z.div_mod_to_quot_rem stronger
Jason Gross
2018-07-10
*
Allow printing more easily readable code in errors
Jason Gross
2018-07-09
*
Prove that to_bytesmod partitions
Jason Gross
2018-07-08
*
Shuffle some ZUtil lemmas around
Jason Gross
2018-07-08
*
Factor eval_reduce_square_exact a bit differently
Jason Gross
2018-07-03
*
Remove nested proofs
Jason Gross
2018-07-03
*
Fix hints, hopefully
Jason Gross
2018-07-03
*
clean
Jason Gross
2018-07-03
[prev]
[next]