Agda Datatypes and Records Index

This page lists all datatypes and records defined in the Agda modules, organized by module.

AVM › Examples

• AccountMsg
• AccountOutput
• CounterMsg
• Key
• KVEvent
• KVMsg

AVM › Instruction

• ConstraintId (record)
• ConstraintInstruction
• ControllerInstruction
• Instruction
• Instr₀
• Instr₁
• Instr₂
• Instr₄
• IntrospectInstruction
• LinearConstraint
• MachineInstruction
• NondetInstruction
• ObjInstruction
• PureInstruction
• Safety
• TxInstruction
• WeightedVal (record)

AVM › Objects

• _→*[_]_
• _→[_]_
• Object (record)
• SequentialObject (record)
• WellFormedObjectType (record)

AVM › Runtime

• AVMError
• BaseError
• DistribError
• EventType
• IntrospectError
• LogEntry (record)
• ObjectMeta (record)
• ObjError
• PureError
• PureLayerError
• Result
• State (record)
• Store (record)
• Success (record)
• TxError
• TxLayerError

Foundation › BasicTypes

• _+_
• _×_
• _↔_ (record)
• _∈_
• _≡_
• Bool
• Dec
• List
• Maybe
• RawMonad (record)
• Σ (record)
• ℕ
• ⊤ (record)
• ⊥

Foundation › Hyperproperties

• _⊑_
• Stream (record)
• System (record)
• Sys× (record)

Foundation › InteractionTrees

• _≈_
• ITree (record)
• ITreeF
• ITree₁ (record)
• MessageEvent

RM › Types › Action

• Action (record)
• DeletionCriterion
• LogicVerifierInput (record)
• Tag

RM › Types › Compliance

• ComplianceInstance (record)
• ComplianceUnit (record)
• ComplianceWitness (record)

RM › Types › ConsumedCreated

• ConsumedCreated

RM › Types › Crypto

• Digest
• PrivateKey
• PublicKey
• Signature

RM › Types › Delta

• DeltaWitness (record)

RM › Types › Identities

• Backend
• Capabilities
• IDParams

RM › Types › Logic

• Logic (record)
• LogicArgs (record)

RM › Types › Nonce

• Nonce (record)

RM › Types › Nullifier

• Nullifier

RM › Types › NullifierKey

• NullifierKey
• NullifierKeyCommitment
• NullifierKeyMatchesCommitment

RM › Types › Program

• Program
• ProgramError
• ResourceQuery
• StorageValue

RM › Types › Resource

• CanNullifyResource (record)
• LogicRef (record)
• Resource (record)

RM › Types › Transaction

• Transaction (record)

---

References to other modules

This page references the following modules:

• AVM.Examples
  • Symbols: CounterMsg, Key, KVMsg, KVEvent, AccountMsg, AccountOutput, VInt, VBool, VString, VPair, VNil, VList, inc, dec, key, put, del, get, put-event, del-event, depositMsg, withdrawMsg, balanceMsg, ok, error-insufficient, balance-val, withdraw, deposit, ok?, kudosTransfer, abortWithMsg, commitWithResult, handleDeposit, handleWithdraw, createCounter, counterExample, handleResult, updateBalance, invalidMsg, helper, handleUpdateResult, updateHelper, transferBatch, processTransfers, closeAccount, closeWithBalance, handleBalance, replay-counter, φ-counter, step-counter, KVStore, apply-kv-event, replay-kv, msg-to-event, φ-kv-aux, φ-kv, step-kv, replay-account, φ-account-aux, φ-account, step-account
• AVM.Instruction
  • Symbols: Safety, ObjInstruction, IntrospectInstruction, Instr₀, TxInstruction, Instr₁, PureInstruction, Instr₂, MachineInstruction, ControllerInstruction, Instruction, NondetInstruction, LinearConstraint, ConstraintInstruction, Instr₄, WeightedVal, ConstraintId, Safe, Unsafe, createObj, destroyObj, call, self, input, getCurrentMachine, reflect, scryMeta, scryDeep, Obj, Introspect, beginTx, commitTx, abortTx, Tx, callPure, registerPure, Pure, getMachine, teleport, moveObject, getCurrentController, getController, transferObject, getCurrentVersion, switchVersion, Machine, Controller, obj-create, obj-destroy, obj-call, get-self, get-input, get-current-machine, obj-scry-meta, obj-scry-deep, obj-reflect, tx-begin, tx-commit, tx-abort, call-pure, register-pure, get-machine, do-teleport, move-object, get-current-controller, get-controller, transfer-object, get-current-version, switch-version, choose, require, mkCid, UseOnce, newConstraint, satisfy, Nondet, Constr, ISA, AVMProgram₀, AVMProgram₁, AVMProgram₂, AVMProgram, AVMProgram₄
• AVM.Objects
  • Symbols: →[]_, →*[]_, Object, WellFormedObjectType, SequentialObject, mkObjType, wfObjType, mkObj, transition, ε-trans, step-trans, InputSequence, ε, is-defined, output-of, ≈φ-refl, ≈φ-sym, ≈φ-trans, BehaviouralState, output, process-input, can-process, ≈ᵒ-refl, ≈ᵒ-sym, ≈ᵒ-trans, ≈ˢ-refl, ≈ˢ-sym, ≈ˢ-trans, behavioural-state-equiv, counter-type, counter-wf, counter-always-defined, prefix-def, echo-type, transition-preserves-type, reachable-from, create-object, initial-output, counter-object, process-preserves-wf, equiv-preserved, equiv-after-input, ·-++-assoc, ObjectBehaviour, execute-step, objecttype-to-behaviour, run-object-itree, ·, ≈φ[]_, ≈ᵒ, ≈ˢ
• AVM.Runtime
  • Symbols: Message, Input, Output, ObjError, IntrospectError, TxError, DistribError, PureError, BaseError, TxLayerError, PureLayerError, AVMError, EventType, Result, ObjectMeta, Store, State, LogEntry, Success, mkMeta, mkStore, ErrObjectNotFound, ErrObjectAlreadyDestroyed, ErrObjectAlreadyExists, ErrInvalidInput, ErrObjectRejectedCall, ErrMetadataCorruption, ErrStoreCorruption, ErrTxConflict, ErrTxNotFound, ErrTxAlreadyCommitted, ErrTxAlreadyAborted, ErrNoActiveTx, ErrInvalidDuringTx, ErrControllerUnreachable, ErrUnauthorizedTransfer, ErrVersionMismatch, ErrCrossControllerTx, ErrMachineUnreachable, ErrInvalidMachineTransfer, ErrFunctionNotFound, ErrFunctionAlreadyRegistered, obj-error, introspect-error, base-error, tx-error, tx-layer-error, pure-error, pure-layer-error, distrib-error, err-object-not-found, err-object-destroyed, err-object-exists, err-invalid-input, err-object-rejected, err-metadata-corruption, err-store-corruption, err-tx-conflict, err-tx-not-found, err-tx-committed, err-tx-aborted, err-no-active-tx, err-invalid-during-tx, err-function-not-found, err-function-registered, err-controller-unreachable, err-unauthorized-transfer, err-version-mismatch, err-cross-controller-tx, err-machine-unreachable, err-invalid-machine-transfer, ObjectCreated, ObjectDestroyed, ObjectCalled, ObjectMoved, ExecutionMoved, ObjectTransferred, ControllerSwitched, TransactionStarted, TransactionCommitted, TransactionAborted, ErrorOccurred, mkLogEntry, mkSuccess, success, failure, ObjectStore, MetaStore, TxWrite, PureFunctions, Trace, BaseResult, TxResult, PureResult, AVMResult
• Foundation.BasicTypes
  • Symbols: ×, +, ⊥, Bool, ≡, Dec, Maybe, ℕ, List, ∈, Σ, ⊤, ↔, RawMonad, ,, ,Σ, inl, inr, tt, true, false, refl, yes, no, nothing, just, zero, suc, [], ∷, here, there, mk↔, fst, snd, ∃, ∃-syntax, ⊥-elim, ¬, not, sym, trans, cong, just≢nothing, just-injective, map-maybe, length, ++-assoc, ++-right-id, map, foldr, null, head, filter, FinSet, Pred, elem, concat, hasDuplicates, concatMap, all, case_of_, ∧, ∨, if_then_else_, ≢, begin_, ≡⟨⟩, ≡⟨⟩_, _∎, >>=ᴹ, +ℕ, *ℕ, ∸, ≥, ≤, ≤?, <?, ≟ℕ, ++, ∈Pred, ⊆, ∘, >>, ==ℕ, ||
• Foundation.Hyperproperties
  • Symbols: lsuc, ⊑, Stream, System, Sys×, []-⊑, ∷-⊑, size, TraceFin, TraceInf, TraceProp, HyperProp, SysAsProp, Obs, Hypersafety, kSafety, α⋆, ⊨, ⊨ᴴ, [_], ≤ᴼ, ⊨α
• Foundation.InteractionTrees
  • Symbols: _, Set₁, MessageEvent, ITreeF, ≈, ITree₁, ITree, send, receive, create, destroy, retF, tauF, visF, ret-eq, tau-left, tau-right, vis-eq, EventSig, Interface, ret, tau, vis, trigger, bind-step, ITree-Monad, Handler, Impl, interp, interp-step, >>=, <$>, first-definition
• RM.Types.Action
  • Symbols: Tag, DeletionCriterion, LogicVerifierInput, Action, DeleteImmediately, StoreForever, LogicVKOuterHash
• RM.Types.Compliance
  • Symbols: ComplianceWitness, ComplianceInstance, ComplianceUnit, MerklePath, ComplianceProof, createComplianceUnit
• RM.Types.ConsumedCreated
  • Symbols: Created, Consumed, ConsumedCreated, isCreated, isConsumed
• RM.Types.Crypto
  • Symbols: PublicKey, PrivateKey, Signature, Digest, curve25519PubKey, curve25519PrivKey, ed25519Signature, Blake3Digest
• RM.Types.Delta
  • Symbols: DeltaWitness, DeltaProof, fromComplianceWitnesses, compose, empty
• RM.Types.Identities
  • Symbols: NodeId, ObjectId, IDParams, Backend, Capabilities, Ed25519, Secp256k1, BLS, localMemory, localConnection, remoteConnection, commit, commitAndDecrypt, Ciphertext, Plaintext, Signable, ExternalId, InternalId, Identity, Commitment, EngineName, ExternalIdentity, EngineId, isLocalEngineID, isRemoteEngineID
• RM.Types.Logic
  • Symbols: LogicArgs, Logic, isConsumedArgs
• RM.Types.Nonce
  • Symbols: Nonce, defaultNonce
• RM.Types.Nullifier
  • Symbols: Nullifier, privateMk, toNonce
• RM.Types.NullifierKey
  • Symbols: NullifierKey, NullifierKeyCommitment, NullifierKeyMatchesCommitment, universal, secret, ofSecret, checkNullifierKey, commitment
• RM.Types.Program
  • Symbols: decrypt, StorageValue, ResourceQuery, ProgramError, Program, str, int, bool, bytes, queryByObjectId, networkError, engineError, decryptionError, commitmentError, identityError, storageError, typeError, userError, skip, raise, tryCatch, withRandomGen, queryResource, submitTransaction, requestCommitment, generateIdentity, connectIdentity, deleteIdentity, getValue, setValue, deleteValue, StorageKey, genObjectId
• RM.Types.Resource
  • Symbols: LogicRef, Resource, CanNullifyResource, isEphemeral, isPersistent, nullifier
• RM.Types.Transaction
  • Symbols: Set, Transaction, generateDeltaProof

?>