diff options
| author |  Robert Sloan <varomodt@gmail.com> | 2016-06-23 00:42:01 -0400 |
|---|---|---|
| committer | Robert Sloan <varomodt@gmail.com> | 2016-06-23 00:42:01 -0400 |
| commit | 8eba1b5866af0ec50c815d88f22198a88ac541dd (patch) | |
| tree | fcefa0b9318ae31fdb0f6aaf300426fc6608a0c8 /src/Assembly/Pipeline.v | |
| parent | 65c3c384aec8216d4d7f9a6fc50d83201035daf5 (diff) | |
Integrate Pseudize into Pipeline.v
Diffstat (limited to 'src/Assembly/Pipeline.v')
| -rw-r--r-- | src/Assembly/Pipeline.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/Assembly/Pipeline.v b/src/Assembly/Pipeline.v index da4df63b7..9299d9d52 100644 --- a/src/Assembly/Pipeline.v +++ b/src/Assembly/Pipeline.v @@ -1,3 +1,4 @@ +Require Import Bedrock.Word. Require Import QhasmCommon QhasmEvalCommon. Require Import Pseudo Qhasm AlmostQhasm Conversion Language. Require Import PseudoConversion AlmostConversion StringConversion. @@ -21,7 +22,7 @@ Module Pipeline. End Pipeline. Module PipelineExample. - Import Pipeline. + Import Pipeline ListNotations. Local Notation "v [[ i ]]" := (nth i v (wzero _)) (at level 40). Local Notation "$$ v" := (natToWord _ v) (at level 40). @@ -35,7 +36,7 @@ Module PipelineExample. pseudo_solve. Defined. - Definition exStr := Pipeline.toString example. + Definition exStr := Pipeline.toString (proj1_sig example). (* Eval vm_compute in exStr. *) End PipelineExample. |