Consumed Created

view source: ConsumedCreated.lagda.md

This module defines the ConsumedCreated type representing whether a resource is consumed or created.

{-# OPTIONS --without-K #-}

module Goose.Anoma.ConsumedCreated where

open import Foundation.BasicTypes 

Consumed Created Type

data ConsumedCreated : Set where
  Created  : ConsumedCreated
  Consumed : ConsumedCreated

Predicates

isCreated : ConsumedCreated → Bool
isCreated Created  = true
isCreated Consumed = false

isConsumed : ConsumedCreated → Bool
isConsumed Consumed = true
isConsumed Created  = false

---

Module References

Referenced By

This module is referenced by:

• Goose.Anoma.Action
  • Symbols: ConsumedCreated
• Goose.Anoma.Logic
  • Symbols: ConsumedCreated, isConsumed

References

This module references:

• Foundation.BasicTypes
  • Imports: Bool, false, true