Logic

view source: Logic.lagda.md

Resource logic structures for the Anoma Resource Machine.

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

module Goose.Anoma.Logic where

open import Foundation.BasicTypes 
open import Goose.Anoma.Resource
open import Goose.Anoma.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:

• Foundation.BasicTypes
  • Imports: Bool, List
• Goose.Anoma.ConsumedCreated
  • Imports: ConsumedCreated, isConsumed
• Goose.Anoma.Resource
  • Imports: LogicRef, Resource