johnchandlerburnham

W(A : Type, B : A -> Type) : Type
  w<P : W(A,B) -> Type> ->
  (sup : (x: A, f: B(x) -> W(A,B)) -> P(W.sup<A,B>(x,f))) ->
  P(w)

W.sup<A: Type, B: A -> Type>(x: A, f: B(x) -> W(A,B)) : W(A,B)
  <P> (sup) sup(x,f)

T Two
| t0;

johnchandlerburnham

{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE MultiWayIf #-}
module Wau where

import           Data.Map                       (Map)
import qualified Data.Map                       as M
import           Data.Maybe                     (isJust)
import           Data.Set                       (Set)
import qualified Data.Set                       as Set
import           Data.STRef

johnchandlerburnham

package example_contract
  open introit
  open contract
  lang contract
where

// pure datatypes are defined outside of contracts
data SimpleToken {
  value: Integer,
  mintedBy: Address,