Agda Datatypes and Records Index

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

AVM › Bytecode

• Bytecode
• DecodeResult
• Opcode

AVM › Instruction

• AVMEvent (record)
• Ctx (record)
• Instr₀
• Object (record)
• Safety
• State (record)
• Val

AVM › Objects

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

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

Goose › Anoma › Action

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

Goose › Anoma › Compliance

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

Goose › Anoma › ConsumedCreated

• ConsumedCreated

Goose › Anoma › Crypto

• Digest
• PrivateKey
• PublicKey
• Signature

Goose › Anoma › Delta

• DeltaWitness (record)

Goose › Anoma › Identities

• Backend
• Capabilities
• IDParams

Goose › Anoma › Logic

• Logic (record)
• LogicArgs (record)

Goose › Anoma › Nonce

• Nonce (record)

Goose › Anoma › Nullifier

• Nullifier

Goose › Anoma › NullifierKey

• NullifierKey
• NullifierKeyCommitment
• NullifierKeyMatchesCommitment

Goose › Anoma › Program

• Program
• ProgramError
• ResourceQuery
• StorageValue

Goose › Anoma › Resource

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

Goose › Anoma › Transaction

• Transaction (record)

---

References to other modules

This page references the following modules:

• AVM.Bytecode
  • Symbols: Opcode, Bytecode, DecodeResult, OP_BEGIN_TX, OP_COMMIT_TX, OP_ABORT_TX, OP_CREATE_OBJ, OP_DESTROY_OBJ, OP_CALL, OP_SCRY, OP_REFLECT, OP_SELF, OP_INPUT, BC, SafeOp, UnsafeOp, TypeError, encode, decode, decodeCommit, decodeScry
• AVM.Instruction
  • Symbols: Val, Safety, Instr₀, Object, Ctx, State, AVMEvent, VInt, VBool, VString, VPair, VNil, VList, ctx, st, ev, Safe, Unsafe, beginTx, commitTx, abortTx, createObj, destroyObj, call, self, input, scry, reflect, Message, Input, Output, Store, TxLog, TxId, Trace, ISA, Filter, AVMProgram, SystemProgram, withdraw, deposit, ok?, kudosTransfer, createCounter, counterExample, updateBalance, invalidMsg, helper, transferBatch, processTransfers, closeAccount, closeWithBalance
• AVM.Objects
  • Symbols: mkObj, →[]_, →*[]_, WellFormedObjectType, SequentialObject, wfObjType, transition, ε-trans, step-trans, InputSequence, ε, ObjectType, 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, ·, ≈φ[]_, ≈ᵒ, ≈ˢ
• 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, FinSet, Pred, 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, _
• Goose.Anoma.Action
  • Symbols: Tag, DeletionCriterion, LogicVerifierInput, Action, DeleteImmediately, StoreForever, LogicVKOuterHash
• Goose.Anoma.Compliance
  • Symbols: ComplianceWitness, ComplianceInstance, ComplianceUnit, MerklePath, ComplianceProof, createComplianceUnit
• Goose.Anoma.ConsumedCreated
  • Symbols: Created, Consumed, ConsumedCreated, isCreated, isConsumed
• Goose.Anoma.Crypto
  • Symbols: PublicKey, PrivateKey, Signature, Digest, curve25519PubKey, curve25519PrivKey, ed25519Signature, Blake3Digest
• Goose.Anoma.Delta
  • Symbols: DeltaWitness, DeltaProof, fromComplianceWitnesses, compose, empty
• Goose.Anoma.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
• Goose.Anoma.Logic
  • Symbols: LogicArgs, Logic, isConsumedArgs
• Goose.Anoma.Nonce
  • Symbols: Nonce, defaultNonce
• Goose.Anoma.Nullifier
  • Symbols: Nullifier, privateMk, toNonce
• Goose.Anoma.NullifierKey
  • Symbols: NullifierKey, NullifierKeyCommitment, NullifierKeyMatchesCommitment, universal, secret, ofSecret, checkNullifierKey, commitment
• Goose.Anoma.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
• Goose.Anoma.Resource
  • Symbols: LogicRef, Resource, CanNullifyResource, isEphemeral, isPersistent, nullifier
• Goose.Anoma.Transaction
  • Symbols: Set, Transaction, generateDeltaProof

?>