examples - 0.0.0

Anoma.Transaction

Description

Definitions

module KindSource#

module PrivateSource#

type KindSource#

Constructors

| mk {id : Nat}

instance Kind-Eq : Eq KindSource#

instance Kind-Ord : Ord KindSource#

open Private using {Kind} public

syntax alias Eq := Private.Kind-EqSource#

open Kind using {Kind} public

module DeltaSource#

module PrivateSource#

type DeltaSource#

Constructors

| mk {unDelta : Map Kind Int}

open Private using {Delta; mk} public

quantity (d : Kind) (delta : Delta) : IntSource#

isBalanced (delta : Delta) : BoolSource#

toList (delta : Delta) : List (Kind × Int)Source#

open Delta using {Delta} public

module HelperSource#

syntax alias Proof := ResourceSource#

syntax alias Commitment := NatSource#

syntax alias Nullifier := NatSource#

positive type ResourceSource#

Constructors

| mkResource { logic : Resource -> Transaction -> Bool; label : Nat; quantity : Nat; data : Nat; eph : Bool; nonce : Nat; npk : Nat; rseed : Nat }

type TransactionSource#

Constructors

| mkTransaction { roots : List Nat; commitments : List Commitment; nullifiers : List Nullifier; proofs : List Proof; delta : Delta; extra : Nat; preference : Nat }

module TransactionSource#

syntax alias mk := Helper.mkTransactionSource#

open Helper.Transaction public

open Helper using {Transaction; Commitment; Nullifier} public

open Transaction using {Transaction; Commitment; Nullifier} public

module ResourceSource#

syntax alias mk := Helper.mkResourceSource#

open Helper.Resource public

open Helper using {Resource} public

open Resource using {Resource} public