{-# OPTIONS --safe --cubical #-}

module Consumer where

open import Spartan6.API.Circuit
open Expression
open Design

consumerInput : Expr 1 0
consumerInput = input fzero

consumerInverter : Design 1 1 0
consumerInverter =
  combinationalDesign (invert consumerInput ∷ [])

consumer-package-reduces :
  observe consumerInverter (low ∷ []) [] ≡ high ∷ []
consumer-package-reduces = refl