module SMT.Unsafe.ShowcaseAssume where

open import Cubical.Foundations.Prelude

open import SMT.Core using (Statement)
open import SMT.Examples.Showcase
open import SMT.Unsafe.Z3

clamp-between-type : Type₀
clamp-between-type = z3CheckedStatement valid-clamp-between

clamp-between-type-ok :
  clamp-between-type ≡ Statement valid-clamp-between
clamp-between-type-ok = refl

overlapping-interval-meet-type : Type₀
overlapping-interval-meet-type =
  z3CheckedStatement valid-overlapping-interval-meet

overlapping-interval-meet-type-ok :
  overlapping-interval-meet-type ≡ Statement valid-overlapping-interval-meet
overlapping-interval-meet-type-ok = refl

absolute-difference-window-type : Type₀
absolute-difference-window-type =
  z3CheckedStatement valid-absolute-difference-window

absolute-difference-window-type-ok :
  absolute-difference-window-type ≡ Statement valid-absolute-difference-window
absolute-difference-window-type-ok = refl

mode-selected-load-bounded-type : Type₀
mode-selected-load-bounded-type =
  z3CheckedStatement valid-mode-selected-load-bounded

mode-selected-load-bounded-type-ok :
  mode-selected-load-bounded-type ≡ Statement valid-mode-selected-load-bounded
mode-selected-load-bounded-type-ok = refl