examples - 0.0.0

Kudos.IntentDsl

Description

A DSL for constructing Kudos exchange intents

Definitions

import Anoma open public

import Kudos.ExampleKinds open public

type QuantifierSource#

Constructors

| Any
| All

type QuantifiedAssetsSource#

Constructors

| mkAssets { quantifier : Quantifier; assets : List Asset }

syntax alias of_ := mkAssetSource#

type IntentionSource#

Constructors

| Want
| Give

type ClauseSource#

Constructors

| mkClause { lhs : Intention × QuantifiedAssets; rhs : QuantifiedAssets }

any (as : List Asset) : QuantifiedAssetsSource#

all (as : List Asset) : QuantifiedAssetsSource#

exactly (a : Asset) : QuantifiedAssetsSource#

want (a : QuantifiedAssets) : Intention × QuantifiedAssetsSource#

give (a : QuantifiedAssets) : Intention × QuantifiedAssetsSource#

for (l : Intention × QuantifiedAssets) (qs : QuantifiedAssets) : ClauseSource#

kudosIntent (clauses : List Clause) : TransactionSource#

axiom mkKudosIntent : List Clause -> TransactionSource#