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
9050
log
plain
-rw-r--r--
Conversion.v
4013
log
plain
-rw-r--r--
CountLets.v
2523
log
plain
-rw-r--r--
Equality.v
4227
log
plain
-rw-r--r--
Eta.v
2827
log
plain
-rw-r--r--
EtaInterp.v
4172
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
4196
log
plain
-rw-r--r--
InlineCast.v
4038
log
plain
-rw-r--r--
InlineCastInterp.v
5761
log
plain
-rw-r--r--
InlineCastWf.v
5326
log
plain
-rw-r--r--
InlineInterp.v
5443
log
plain
-rw-r--r--
InlineWf.v
9490
log
plain
-rw-r--r--
InputSyntax.v
11143
log
plain
-rw-r--r--
InterpByIso.v
1566
log
plain
-rw-r--r--
InterpByIsoProofs.v
5312
log
plain
-rw-r--r--
InterpProofs.v
2400
log
plain
-rw-r--r--
InterpWf.v
2897
log
plain
-rw-r--r--
InterpWfRel.v
4198
log
plain
-rw-r--r--
Linearize.v
2524
log
plain
-rw-r--r--
LinearizeInterp.v
3136
log
plain
-rw-r--r--
LinearizeWf.v
8409
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
17637
log
plain
-rw-r--r--
Relations.v
17957
log
plain
-rw-r--r--
Rewriter.v
1524
log
plain
-rw-r--r--
RewriterInterp.v
2060
log
plain
-rw-r--r--
RewriterWf.v
2330
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
1800
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
6858
log
plain
-rw-r--r--
WfProofs.v
9850
log
plain
-rw-r--r--
WfReflective.v
13841
log
plain
-rw-r--r--
WfReflectiveGen.v
16748
log
plain
d---------
Z
781
log
plain