index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
Reflection
Mode
Name
Size
-rw-r--r--
BoundByCast.v
2335
log
plain
-rw-r--r--
BoundByCastInterp.v
6871
log
plain
-rw-r--r--
BoundByCastWf.v
2166
log
plain
-rw-r--r--
CommonSubexpressionElimination.v
9054
log
plain
-rw-r--r--
Conversion.v
4040
log
plain
-rw-r--r--
CountLets.v
2523
log
plain
-rw-r--r--
Equality.v
4227
log
plain
-rw-r--r--
Eta.v
3355
log
plain
-rw-r--r--
EtaInterp.v
4714
log
plain
-rw-r--r--
EtaWf.v
4798
log
plain
-rw-r--r--
ExprInversion.v
9592
log
plain
-rw-r--r--
FilterLive.v
2865
log
plain
-rw-r--r--
FoldTypes.v
1577
log
plain
-rw-r--r--
Inline.v
4160
log
plain
-rw-r--r--
InlineCast.v
4038
log
plain
-rw-r--r--
InlineCastInterp.v
5886
log
plain
-rw-r--r--
InlineCastWf.v
5326
log
plain
-rw-r--r--
InlineInterp.v
5661
log
plain
-rw-r--r--
InlineWf.v
9490
log
plain
-rw-r--r--
InputSyntax.v
11154
log
plain
-rw-r--r--
InterpByIso.v
1566
log
plain
-rw-r--r--
InterpByIsoProofs.v
5312
log
plain
-rw-r--r--
InterpProofs.v
2569
log
plain
-rw-r--r--
InterpWf.v
3006
log
plain
-rw-r--r--
InterpWfRel.v
4211
log
plain
-rw-r--r--
Linearize.v
2528
log
plain
-rw-r--r--
LinearizeInterp.v
3401
log
plain
-rw-r--r--
LinearizeWf.v
8413
log
plain
-rw-r--r--
Map.v
1260
log
plain
-rw-r--r--
MapCast.v
5093
log
plain
-rw-r--r--
MapCastByDeBruijn.v
3226
log
plain
-rw-r--r--
MapCastByDeBruijnInterp.v
6534
log
plain
-rw-r--r--
MapCastByDeBruijnWf.v
5815
log
plain
-rw-r--r--
MapCastInterp.v
12009
log
plain
-rw-r--r--
MapCastWf.v
6510
log
plain
-rw-r--r--
MultiSizeTest.v
7485
log
plain
-rw-r--r--
MultiSizeTest2.v
5724
log
plain
d---------
Named
1146
log
plain
-rw-r--r--
Reify.v
17714
log
plain
-rw-r--r--
Relations.v
18068
log
plain
-rw-r--r--
RenameBinders.v
3073
log
plain
-rw-r--r--
Rewriter.v
1542
log
plain
-rw-r--r--
RewriterInterp.v
2129
log
plain
-rw-r--r--
RewriterWf.v
2318
log
plain
-rw-r--r--
SmartBound.v
6884
log
plain
-rw-r--r--
SmartBoundInterp.v
7871
log
plain
-rw-r--r--
SmartBoundWf.v
6251
log
plain
-rw-r--r--
SmartCast.v
1630
log
plain
-rw-r--r--
SmartCastInterp.v
1895
log
plain
-rw-r--r--
SmartCastWf.v
3684
log
plain
-rw-r--r--
SmartMap.v
17346
log
plain
-rw-r--r--
Syntax.v
6097
log
plain
-rw-r--r--
TestCase.v
11212
log
plain
-rw-r--r--
Tuple.v
3202
log
plain
-rw-r--r--
TypeInversion.v
7642
log
plain
-rw-r--r--
TypeUtil.v
1427
log
plain
-rw-r--r--
Wf.v
3224
log
plain
-rw-r--r--
WfInversion.v
6918
log
plain
-rw-r--r--
WfProofs.v
9977
log
plain
-rw-r--r--
WfReflective.v
13917
log
plain
-rw-r--r--
WfReflectiveGen.v
16775
log
plain
d---------
Z
826
log
plain