Anoma - Resource Machine Data Types

view source: Types.lagda.md

This module provides the main entry point for the Anoma Resource Machine components.

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

module RM.Types where

open import RM.Types.ConsumedCreated public
open import RM.Types.Crypto public
open import RM.Types.Identities public
open import RM.Types.NullifierKey public
open import RM.Types.Nonce public
open import RM.Types.Nullifier public
open import RM.Types.Resource public
open import RM.Types.Logic public
open import RM.Types.Compliance public
open import RM.Types.Delta public
open import RM.Types.Action public
open import RM.Types.Transaction public
open import RM.Types.Program public