src/RewriterProofs.v


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24

Require Import Crypto.Rewriter.NBE.
Require Import Crypto.Rewriter.Arith.
Require Import Crypto.Rewriter.ArithWithCasts.
Require Import Crypto.Rewriter.StripLiteralCasts.
Require Import Crypto.Rewriter.ToFancy.
Require Import Crypto.Rewriter.ToFancyWithCasts.

Module Compilers.
  Export NBE.Compilers.
  Export Arith.Compilers.
  Export ArithWithCasts.Compilers.
  Export StripLiteralCasts.Compilers.
  Export ToFancy.Compilers.
  Export ToFancyWithCasts.Compilers.

  Module Import RewriteRules.
    Export NBE.Compilers.RewriteRules.
    Export Arith.Compilers.RewriteRules.
    Export ArithWithCasts.Compilers.RewriteRules.
    Export StripLiteralCasts.Compilers.RewriteRules.
    Export ToFancy.Compilers.RewriteRules.
    Export ToFancyWithCasts.Compilers.RewriteRules.
  End RewriteRules.
End Compilers.