index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
Compilers
Mode
Name
Size
-rw-r--r--
CommonSubexpressionElimination.v
11325
log
plain
-rw-r--r--
CommonSubexpressionEliminationDenote.v
6291
log
plain
-rw-r--r--
CommonSubexpressionEliminationInterp.v
10744
log
plain
-rw-r--r--
CommonSubexpressionEliminationProperties.v
11123
log
plain
-rw-r--r--
CommonSubexpressionEliminationWf.v
12792
log
plain
-rw-r--r--
Conversion.v
4098
log
plain
-rw-r--r--
CountLets.v
2521
log
plain
-rw-r--r--
Equality.v
4236
log
plain
-rw-r--r--
Eta.v
3353
log
plain
-rw-r--r--
EtaInterp.v
5747
log
plain
-rw-r--r--
EtaWf.v
4891
log
plain
-rw-r--r--
ExprInversion.v
13749
log
plain
-rw-r--r--
FilterLive.v
2861
log
plain
-rw-r--r--
FoldTypes.v
1574
log
plain
-rw-r--r--
GeneralizeVar.v
1850
log
plain
-rw-r--r--
GeneralizeVarInterp.v
3874
log
plain
-rw-r--r--
GeneralizeVarWf.v
3594
log
plain
d---------
InSet
116
log
plain
-rw-r--r--
Inline.v
4627
log
plain
-rw-r--r--
InlineConstAndOp.v
6791
log
plain
-rw-r--r--
InlineConstAndOpByRewrite.v
4113
log
plain
-rw-r--r--
InlineConstAndOpByRewriteInterp.v
6050
log
plain
-rw-r--r--
InlineConstAndOpByRewriteWf.v
7890
log
plain
-rw-r--r--
InlineConstAndOpInterp.v
6978
log
plain
-rw-r--r--
InlineConstAndOpWf.v
9753
log
plain
-rw-r--r--
InlineInterp.v
5807
log
plain
-rw-r--r--
InlineWf.v
9904
log
plain
-rw-r--r--
InputSyntax.v
11245
log
plain
-rw-r--r--
InterpByIso.v
1563
log
plain
-rw-r--r--
InterpByIsoProofs.v
5436
log
plain
-rw-r--r--
InterpProofs.v
2609
log
plain
-rw-r--r--
InterpRewriting.v
7666
log
plain
-rw-r--r--
InterpSideConditions.v
2090
log
plain
-rw-r--r--
InterpWf.v
3036
log
plain
-rw-r--r--
InterpWfRel.v
4255
log
plain
-rw-r--r--
Intros.v
3868
log
plain
-rw-r--r--
Linearize.v
4684
log
plain
-rw-r--r--
LinearizeInterp.v
5834
log
plain
-rw-r--r--
LinearizeWf.v
7271
log
plain
-rw-r--r--
Map.v
1259
log
plain
-rw-r--r--
MapBaseType.v
4847
log
plain
-rw-r--r--
MapBaseTypeWf.v
4907
log
plain
-rw-r--r--
MapCastByDeBruijn.v
3265
log
plain
-rw-r--r--
MapCastByDeBruijnInterp.v
7431
log
plain
-rw-r--r--
MapCastByDeBruijnWf.v
5944
log
plain
-rw-r--r--
MultiSizeTest.v
7456
log
plain
d---------
Named
1735
log
plain
-rw-r--r--
Reify.v
27349
log
plain
-rw-r--r--
Relations.v
18312
log
plain
-rw-r--r--
RenameBinders.v
3071
log
plain
-rw-r--r--
Rewriter.v
1541
log
plain
-rw-r--r--
RewriterInterp.v
2162
log
plain
-rw-r--r--
RewriterWf.v
2347
log
plain
-rw-r--r--
SmartMap.v
23107
log
plain
-rw-r--r--
StripExpr.v
1148
log
plain
-rw-r--r--
Syntax.v
6171
log
plain
-rw-r--r--
TestCase.v
13103
log
plain
-rw-r--r--
Tuple.v
4154
log
plain
-rw-r--r--
TypeInversion.v
7641
log
plain
-rw-r--r--
TypeUtil.v
1426
log
plain
-rw-r--r--
Wf.v
3207
log
plain
-rw-r--r--
WfInversion.v
7163
log
plain
-rw-r--r--
WfProofs.v
21039
log
plain
-rw-r--r--
WfReflective.v
14089
log
plain
-rw-r--r--
WfReflectiveGen.v
16987
log
plain
d---------
Z
1792
log
plain
d---------
ZExtended
429
log
plain