File tree Expand file tree Collapse file tree 2 files changed +2
-2
lines changed
formal-spec/Leios/Foreign Expand file tree Collapse file tree 2 files changed +2
-2
lines changed Original file line number Diff line number Diff line change @@ -18,7 +18,7 @@ open Equivalence
1818
1919-- The module contains very simple implementations for the functionalities
2020-- that allow to build examples for traces for the different Leios variants
21- module Leios.Trace where
21+ module Leios.Foreign.Defaults where
2222
2323instance
2424 htx : Hashable (List ℕ) String
Original file line number Diff line number Diff line change @@ -10,7 +10,7 @@ open import Tactic.Derive.Convertible
1010open import Tactic.Derive.HsType
1111
1212open import Leios.Prelude
13- open import Leios.Trace renaming (EndorserBlock to EndorserBlockAgda; IBHeader to IBHeaderAgda)
13+ open import Leios.Foreign.Defaults renaming (EndorserBlock to EndorserBlockAgda; IBHeader to IBHeaderAgda)
1414open import Leios.Foreign.BaseTypes
1515open import Leios.Foreign.HSTypes
1616open import Leios.Foreign.Util
You can’t perform that action at this time.
0 commit comments