examples - 0.0.0

Anoma.Internal.Transaction

Description

Definitions

module DeltaComponentSource#

type DeltaComponentSource#

Constructors

| mk { denom : Nat; sign : Bool; amount : Nat }

zero : DeltaComponentSource#

open DeltaComponent public

open DeltaComponent using {DeltaComponent} public

Delta : TypeSource#

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} public

open Transaction using {Transaction} public

module ResourceSource#

syntax alias mk := Helper.mkResourceSource#

open Helper.Resource public

open Helper using {Resource} public

open Resource using {Resource} public