Skip to content

Logic

Resource logic structures for the Anoma Resource Machine.

{-# OPTIONS --without-K --type-in-type #-}

module RM.Types.Logic where

open import Foundation.BasicTypes
open import RM.Types.Resource
open import RM.Types.ConsumedCreated

Logic Arguments

record LogicArgs : Set where
  field
    self : Resource
    status : ConsumedCreated
    consumed : List Resource
    created : List Resource
    Data : Set
    appData : Data

open LogicArgs public

Logic Arguments Predicate

isConsumedArgs : LogicArgs → Bool
isConsumedArgs args = isConsumed (args .status)

Logic Structure

record Logic : Set where
  field
    reference : LogicRef
    function : LogicArgs → Bool

open Logic public
Module References

References

This module references: