diff options
| author |  Jason Gross <jasongross9@gmail.com> | 2016-09-29 00:02:59 -0400 |
|---|---|---|
| committer |  GitHub <noreply@github.com> | 2016-09-29 00:02:59 -0400 |
| commit | 5f5c21a0f97a5ea6bf65893173e768db2865235d (patch) | |
| tree | 32b414b6d21f05d72577607e7961b16c3bc0ef1b /_CoqProject | |
| parent | 6421648fa427497cbcbb75936e6206dcabd37c10 (diff) | |
Small example of bounds-calculation with dependent types (#61)
This might properly belong in Experiments rather than TestCase. It demos the
ability to transform from one kind of constants to another kind, and to plug
bounds calculation functions into [var] to get bounds. There's not currently
any sort of correctness theorem, and I'm not entirely sure what one would look
like. Probably something that says that if you map a function over the syntax
tree and then interpret, you could instead have first interpreted and then
applied the function.
I'm hopeful that this will provide a template for integrating this version of
the syntax with rsloan-phoas.
Diffstat (limited to '_CoqProject')
| -rw-r--r-- | _CoqProject | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject index 2a92f9a4e..266006217 100644 --- a/_CoqProject +++ b/_CoqProject @@ -63,6 +63,7 @@ src/ModularArithmetic/Montgomery/Z.v src/ModularArithmetic/Montgomery/ZBounded.v src/ModularArithmetic/Montgomery/ZProofs.v src/Reflection/CommonSubexpressionElimination.v +src/Reflection/Conversion.v src/Reflection/CountLets.v src/Reflection/FilterLive.v src/Reflection/Inline.v |