/src/
../
AbstractInterpretation.v
AbstractInterpretationProofs.v
AbstractInterpretationWf.v
AbstractInterpretationZRangeProofs.v
Algebra
Arithmetic.v
Arithmetic
BoundsPipeline.v
CLI.v
COperationSpecifications.v
CStringification.v
Compilers
CompilersTestCases.v
Curves
Demo.v
Experiments
ExtractionHaskell
ExtractionOCaml
GENERATEDIdentifiersWithoutTypes.v
GENERATEDIdentifiersWithoutTypesProofs.v
Language.v
LanguageInversion.v
LanguageWf.v
LegacyArithmetic
MiscCompilerPasses.v
MiscCompilerPassesProofs.v
Primitives
PushButtonSynthesis.v
PushButtonSynthesis
README.md
Rewriter.v
RewriterInterpProofs1.v
RewriterProofs.v
RewriterRulesGood.v
RewriterRulesInterpGood.v
RewriterWf1.v
RewriterWf2.v
SlowPrimeSynthesisExamples.v
Spec
Specific
StandaloneHaskellMain.v
StandaloneOCamlMain.v
Toplevel2.v
UnderLets.v
UnderLetsProofs.v
Util
arith_rewrite_head.out
arith_with_casts_rewrite_head.out
fancy_rewrite_head.out
fancy_with_casts_rewrite_head.out
haskell.sed
nbe_rewrite_head.out