From 04ea70e2e60cd7014606e725a5b2322687a8af60 Mon Sep 17 00:00:00 2001 From: Jakob von Raumer Date: Mon, 16 Dec 2024 17:01:32 +0100 Subject: [PATCH] ajust expected test outputs --- test/lean/bitvec_operation.expected.lean | 2 +- test/lean/enum.expected.lean | 2 +- test/lean/extern.expected.lean | 2 +- test/lean/let.expected.lean | 2 +- test/lean/struct.expected.lean | 3 ++- test/lean/trivial.expected.lean | 2 +- test/lean/tuples.expected.lean | 2 +- test/lean/typquant.expected.lean | 2 +- 8 files changed, 9 insertions(+), 8 deletions(-) diff --git a/test/lean/bitvec_operation.expected.lean b/test/lean/bitvec_operation.expected.lean index 3807b800a..9d024bd61 100644 --- a/test/lean/bitvec_operation.expected.lean +++ b/test/lean/bitvec_operation.expected.lean @@ -1,4 +1,4 @@ -import Sail.sail +import MyProject.Sail.Sail def bitvector_eq (x : BitVec 16) (y : BitVec 16) : Bool := (Eq x y) diff --git a/test/lean/enum.expected.lean b/test/lean/enum.expected.lean index 2fad5dcfb..a83b0235f 100644 --- a/test/lean/enum.expected.lean +++ b/test/lean/enum.expected.lean @@ -1,4 +1,4 @@ -import Sail.sail +import MyProject.Sail.Sail inductive E where | A | B | C deriving Inhabited diff --git a/test/lean/extern.expected.lean b/test/lean/extern.expected.lean index cb4785ae3..894c4d38a 100644 --- a/test/lean/extern.expected.lean +++ b/test/lean/extern.expected.lean @@ -1,4 +1,4 @@ -import Sail.sail +import MyProject.Sail.Sail def extern_add : Int := (Int.add 5 4) diff --git a/test/lean/let.expected.lean b/test/lean/let.expected.lean index b13e6ae83..31043ac64 100644 --- a/test/lean/let.expected.lean +++ b/test/lean/let.expected.lean @@ -1,4 +1,4 @@ -import Sail.sail +import MyProject.Sail.Sail def foo : BitVec 16 := let z := (HOr.hOr (0xFFFF : BitVec 16) (0xABCD : BitVec 16)) diff --git a/test/lean/struct.expected.lean b/test/lean/struct.expected.lean index 38d801fcd..01e1d41b2 100644 --- a/test/lean/struct.expected.lean +++ b/test/lean/struct.expected.lean @@ -1,4 +1,4 @@ -import My_Project.Sail.sail +import MyProject.Sail.Sail structure My_struct where field1 : Int @@ -10,3 +10,4 @@ def undefined_My_struct (lit : Unit) : My_struct := def initialize_registers : Unit := () + diff --git a/test/lean/trivial.expected.lean b/test/lean/trivial.expected.lean index f7df77729..e96b73304 100644 --- a/test/lean/trivial.expected.lean +++ b/test/lean/trivial.expected.lean @@ -1,4 +1,4 @@ -import Sail.sail +import MyProject.Sail.Sail def foo (y : Unit) : Unit := y diff --git a/test/lean/tuples.expected.lean b/test/lean/tuples.expected.lean index 5ac53560d..d37669d16 100644 --- a/test/lean/tuples.expected.lean +++ b/test/lean/tuples.expected.lean @@ -1,4 +1,4 @@ -import Sail.sail +import MyProject.Sail.Sail def tuple1 : (Int × Int × (BitVec 2 × Unit)) := (3, 5, ((0b10 : BitVec 2), ())) diff --git a/test/lean/typquant.expected.lean b/test/lean/typquant.expected.lean index 4449ad932..4f6d202e9 100644 --- a/test/lean/typquant.expected.lean +++ b/test/lean/typquant.expected.lean @@ -1,4 +1,4 @@ -import Sail.sail +import MyProject.Sail.Sail def foo (n : Int) : BitVec 4 := (0xF : BitVec 4)