diff options
| author |  Robert Sloan <varomodt@gmail.com> | 2016-05-18 22:22:47 -0400 |
|---|---|---|
| committer | Robert Sloan <varomodt@gmail.com> | 2016-05-18 22:22:47 -0400 |
| commit | 093630a451ac5d2ccf5fb5224d99f74bd7a9679d (patch) | |
| tree | a61119cc2cd5c606ff79149d2b9a17aae556a694 /src/Assembly | |
| parent | e4cffa7f54c4d11dd89095c436b7c655a1e3afdb (diff) | |
Tuple-ization tactics work
Diffstat (limited to 'src/Assembly')
| -rw-r--r-- | src/Assembly/Pseudo.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/Assembly/Pseudo.v b/src/Assembly/Pseudo.v index f5baa96c6..06264d10a 100644 --- a/src/Assembly/Pseudo.v +++ b/src/Assembly/Pseudo.v @@ -58,10 +58,10 @@ Module Pseudo (M: PseudoMachine) <: Language. | PVar: forall n, Index n -> Pseudo n 1 | PConst: forall n, const -> Pseudo n 1 - | PBin: forall n, WBinOp -> Pseudo n 1 -> Pseudo n 1 -> Pseudo n 1 + | PBin: forall n, WBinOp -> Pseudo n 2 -> Pseudo n 1 | PNat: forall n, WNatOp -> Index width -> Pseudo n 1 - | PDual: forall n, WDualOp -> Pseudo n 1 -> Pseudo n 1 -> Pseudo n 2 - | PShift: forall n, WShiftOp -> Pseudo n 1 -> Index width -> Pseudo n 1 + | PDual: forall n, WDualOp -> Pseudo n 2 -> Pseudo n 2 + | PShift: forall n, WShiftOp -> Index width -> Pseudo n 1 -> Pseudo n 1 | PLet: forall n k m, Pseudo n k -> Pseudo (n + k) m -> Pseudo n m | PComp: forall n k m, Pseudo n k -> Pseudo k m -> Pseudo n m |