Michelson.Typed.Arith

Module, containing some boilerplate for support of arithmetic operations in Michelson language.

Documentation

class ArithOp aop (n :: T) (m :: T) where

Class for binary arithmetic operation.

Takes binary operation marker as op parameter, types of left operand n and right operand m.

Minimal complete definition

convergeArith, evalOp

Associated Types

type ArithRes aop n m :: T

Type family ArithRes denotes the type resulting from computing operation op from operands of types n and m.

For instance, adding integer to natural produces integer, which is reflected in following instance of type family: ArithRes Add CNat CInt = CInt.

Methods

convergeArith :: proxy aop -> Notes n -> Notes m -> Either AnnConvergeError (Notes (ArithRes aop n m))

Converge the notes of given operands.

evalOp :: proxy aop -> Value' instr n -> Value' instr m -> Either (ArithError (Value' instr n) (Value' instr m)) (Value' instr (ArithRes aop n m))

Evaluate arithmetic operation on given operands.

commutativityProof :: Maybe $ Dict (ArithRes aop n m ~ ArithRes aop m n, ArithOp aop m n)

An operation can marked as commutative, it does not affect its runtime behavior, but enables certain optimization in the optimizer. We conservatively consider operations non-commutative by default.

Note that there is one unusual case: AND works with int : nat but not with nat : int. That's how it's specified in Michelson.

Instances

ArithOp Lsr 'TNat 'TNat

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Lsr 'TNat 'TNat :: T

Methods

convergeArith :: proxy Lsr -> Notes 'TNat -> Notes 'TNat -> Either AnnConvergeError (Notes (ArithRes Lsr 'TNat 'TNat))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Lsr -> Value' instr 'TNat -> Value' instr 'TNat -> Either (ArithError (Value' instr 'TNat) (Value' instr 'TNat)) (Value' instr (ArithRes Lsr 'TNat 'TNat))

commutativityProof :: Maybe $ Dict (ArithRes Lsr 'TNat 'TNat ~ ArithRes Lsr 'TNat 'TNat, ArithOp Lsr 'TNat 'TNat)

ArithOp Lsl 'TNat 'TNat

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Lsl 'TNat 'TNat :: T

Methods

convergeArith :: proxy Lsl -> Notes 'TNat -> Notes 'TNat -> Either AnnConvergeError (Notes (ArithRes Lsl 'TNat 'TNat))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Lsl -> Value' instr 'TNat -> Value' instr 'TNat -> Either (ArithError (Value' instr 'TNat) (Value' instr 'TNat)) (Value' instr (ArithRes Lsl 'TNat 'TNat))

commutativityProof :: Maybe $ Dict (ArithRes Lsl 'TNat 'TNat ~ ArithRes Lsl 'TNat 'TNat, ArithOp Lsl 'TNat 'TNat)

ArithOp Xor 'TNat 'TNat

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Xor 'TNat 'TNat :: T

Methods

convergeArith :: proxy Xor -> Notes 'TNat -> Notes 'TNat -> Either AnnConvergeError (Notes (ArithRes Xor 'TNat 'TNat))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Xor -> Value' instr 'TNat -> Value' instr 'TNat -> Either (ArithError (Value' instr 'TNat) (Value' instr 'TNat)) (Value' instr (ArithRes Xor 'TNat 'TNat))

commutativityProof :: Maybe $ Dict (ArithRes Xor 'TNat 'TNat ~ ArithRes Xor 'TNat 'TNat, ArithOp Xor 'TNat 'TNat)

ArithOp Xor 'TBool 'TBool

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Xor 'TBool 'TBool :: T

Methods

convergeArith :: proxy Xor -> Notes 'TBool -> Notes 'TBool -> Either AnnConvergeError (Notes (ArithRes Xor 'TBool 'TBool))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Xor -> Value' instr 'TBool -> Value' instr 'TBool -> Either (ArithError (Value' instr 'TBool) (Value' instr 'TBool)) (Value' instr (ArithRes Xor 'TBool 'TBool))

commutativityProof :: Maybe $ Dict (ArithRes Xor 'TBool 'TBool ~ ArithRes Xor 'TBool 'TBool, ArithOp Xor 'TBool 'TBool)

ArithOp And 'TInt 'TNat

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes And 'TInt 'TNat :: T

Methods

convergeArith :: proxy And -> Notes 'TInt -> Notes 'TNat -> Either AnnConvergeError (Notes (ArithRes And 'TInt 'TNat))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy And -> Value' instr 'TInt -> Value' instr 'TNat -> Either (ArithError (Value' instr 'TInt) (Value' instr 'TNat)) (Value' instr (ArithRes And 'TInt 'TNat))

commutativityProof :: Maybe $ Dict (ArithRes And 'TInt 'TNat ~ ArithRes And 'TNat 'TInt, ArithOp And 'TNat 'TInt)

ArithOp And 'TNat 'TNat

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes And 'TNat 'TNat :: T

Methods

convergeArith :: proxy And -> Notes 'TNat -> Notes 'TNat -> Either AnnConvergeError (Notes (ArithRes And 'TNat 'TNat))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy And -> Value' instr 'TNat -> Value' instr 'TNat -> Either (ArithError (Value' instr 'TNat) (Value' instr 'TNat)) (Value' instr (ArithRes And 'TNat 'TNat))

commutativityProof :: Maybe $ Dict (ArithRes And 'TNat 'TNat ~ ArithRes And 'TNat 'TNat, ArithOp And 'TNat 'TNat)

ArithOp And 'TBool 'TBool

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes And 'TBool 'TBool :: T

Methods

convergeArith :: proxy And -> Notes 'TBool -> Notes 'TBool -> Either AnnConvergeError (Notes (ArithRes And 'TBool 'TBool))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy And -> Value' instr 'TBool -> Value' instr 'TBool -> Either (ArithError (Value' instr 'TBool) (Value' instr 'TBool)) (Value' instr (ArithRes And 'TBool 'TBool))

commutativityProof :: Maybe $ Dict (ArithRes And 'TBool 'TBool ~ ArithRes And 'TBool 'TBool, ArithOp And 'TBool 'TBool)

ArithOp Or 'TNat 'TNat

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Or 'TNat 'TNat :: T

Methods

convergeArith :: proxy Or -> Notes 'TNat -> Notes 'TNat -> Either AnnConvergeError (Notes (ArithRes Or 'TNat 'TNat))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Or -> Value' instr 'TNat -> Value' instr 'TNat -> Either (ArithError (Value' instr 'TNat) (Value' instr 'TNat)) (Value' instr (ArithRes Or 'TNat 'TNat))

commutativityProof :: Maybe $ Dict (ArithRes Or 'TNat 'TNat ~ ArithRes Or 'TNat 'TNat, ArithOp Or 'TNat 'TNat)

ArithOp Or 'TBool 'TBool

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Or 'TBool 'TBool :: T

Methods

convergeArith :: proxy Or -> Notes 'TBool -> Notes 'TBool -> Either AnnConvergeError (Notes (ArithRes Or 'TBool 'TBool))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Or -> Value' instr 'TBool -> Value' instr 'TBool -> Either (ArithError (Value' instr 'TBool) (Value' instr 'TBool)) (Value' instr (ArithRes Or 'TBool 'TBool))

commutativityProof :: Maybe $ Dict (ArithRes Or 'TBool 'TBool ~ ArithRes Or 'TBool 'TBool, ArithOp Or 'TBool 'TBool)

ArithOp Mul 'TInt 'TInt

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Mul 'TInt 'TInt :: T

Methods

convergeArith :: proxy Mul -> Notes 'TInt -> Notes 'TInt -> Either AnnConvergeError (Notes (ArithRes Mul 'TInt 'TInt))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Mul -> Value' instr 'TInt -> Value' instr 'TInt -> Either (ArithError (Value' instr 'TInt) (Value' instr 'TInt)) (Value' instr (ArithRes Mul 'TInt 'TInt))

commutativityProof :: Maybe $ Dict (ArithRes Mul 'TInt 'TInt ~ ArithRes Mul 'TInt 'TInt, ArithOp Mul 'TInt 'TInt)

ArithOp Mul 'TInt 'TNat

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Mul 'TInt 'TNat :: T

Methods

convergeArith :: proxy Mul -> Notes 'TInt -> Notes 'TNat -> Either AnnConvergeError (Notes (ArithRes Mul 'TInt 'TNat))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Mul -> Value' instr 'TInt -> Value' instr 'TNat -> Either (ArithError (Value' instr 'TInt) (Value' instr 'TNat)) (Value' instr (ArithRes Mul 'TInt 'TNat))

commutativityProof :: Maybe $ Dict (ArithRes Mul 'TInt 'TNat ~ ArithRes Mul 'TNat 'TInt, ArithOp Mul 'TNat 'TInt)

ArithOp Mul 'TNat 'TInt

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Mul 'TNat 'TInt :: T

Methods

convergeArith :: proxy Mul -> Notes 'TNat -> Notes 'TInt -> Either AnnConvergeError (Notes (ArithRes Mul 'TNat 'TInt))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Mul -> Value' instr 'TNat -> Value' instr 'TInt -> Either (ArithError (Value' instr 'TNat) (Value' instr 'TInt)) (Value' instr (ArithRes Mul 'TNat 'TInt))

commutativityProof :: Maybe $ Dict (ArithRes Mul 'TNat 'TInt ~ ArithRes Mul 'TInt 'TNat, ArithOp Mul 'TInt 'TNat)

ArithOp Mul 'TNat 'TNat

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Mul 'TNat 'TNat :: T

Methods

convergeArith :: proxy Mul -> Notes 'TNat -> Notes 'TNat -> Either AnnConvergeError (Notes (ArithRes Mul 'TNat 'TNat))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Mul -> Value' instr 'TNat -> Value' instr 'TNat -> Either (ArithError (Value' instr 'TNat) (Value' instr 'TNat)) (Value' instr (ArithRes Mul 'TNat 'TNat))

commutativityProof :: Maybe $ Dict (ArithRes Mul 'TNat 'TNat ~ ArithRes Mul 'TNat 'TNat, ArithOp Mul 'TNat 'TNat)

ArithOp Mul 'TNat 'TMutez

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Mul 'TNat 'TMutez :: T

Methods

convergeArith :: proxy Mul -> Notes 'TNat -> Notes 'TMutez -> Either AnnConvergeError (Notes (ArithRes Mul 'TNat 'TMutez))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Mul -> Value' instr 'TNat -> Value' instr 'TMutez -> Either (ArithError (Value' instr 'TNat) (Value' instr 'TMutez)) (Value' instr (ArithRes Mul 'TNat 'TMutez))

commutativityProof :: Maybe $ Dict (ArithRes Mul 'TNat 'TMutez ~ ArithRes Mul 'TMutez 'TNat, ArithOp Mul 'TMutez 'TNat)

ArithOp Mul 'TMutez 'TNat

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Mul 'TMutez 'TNat :: T

Methods

convergeArith :: proxy Mul -> Notes 'TMutez -> Notes 'TNat -> Either AnnConvergeError (Notes (ArithRes Mul 'TMutez 'TNat))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Mul -> Value' instr 'TMutez -> Value' instr 'TNat -> Either (ArithError (Value' instr 'TMutez) (Value' instr 'TNat)) (Value' instr (ArithRes Mul 'TMutez 'TNat))

commutativityProof :: Maybe $ Dict (ArithRes Mul 'TMutez 'TNat ~ ArithRes Mul 'TNat 'TMutez, ArithOp Mul 'TNat 'TMutez)

ArithOp Sub 'TInt 'TInt

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Sub 'TInt 'TInt :: T

Methods

convergeArith :: proxy Sub -> Notes 'TInt -> Notes 'TInt -> Either AnnConvergeError (Notes (ArithRes Sub 'TInt 'TInt))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Sub -> Value' instr 'TInt -> Value' instr 'TInt -> Either (ArithError (Value' instr 'TInt) (Value' instr 'TInt)) (Value' instr (ArithRes Sub 'TInt 'TInt))

commutativityProof :: Maybe $ Dict (ArithRes Sub 'TInt 'TInt ~ ArithRes Sub 'TInt 'TInt, ArithOp Sub 'TInt 'TInt)

ArithOp Sub 'TInt 'TNat

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Sub 'TInt 'TNat :: T

Methods

convergeArith :: proxy Sub -> Notes 'TInt -> Notes 'TNat -> Either AnnConvergeError (Notes (ArithRes Sub 'TInt 'TNat))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Sub -> Value' instr 'TInt -> Value' instr 'TNat -> Either (ArithError (Value' instr 'TInt) (Value' instr 'TNat)) (Value' instr (ArithRes Sub 'TInt 'TNat))

commutativityProof :: Maybe $ Dict (ArithRes Sub 'TInt 'TNat ~ ArithRes Sub 'TNat 'TInt, ArithOp Sub 'TNat 'TInt)

ArithOp Sub 'TNat 'TInt

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Sub 'TNat 'TInt :: T

Methods

convergeArith :: proxy Sub -> Notes 'TNat -> Notes 'TInt -> Either AnnConvergeError (Notes (ArithRes Sub 'TNat 'TInt))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Sub -> Value' instr 'TNat -> Value' instr 'TInt -> Either (ArithError (Value' instr 'TNat) (Value' instr 'TInt)) (Value' instr (ArithRes Sub 'TNat 'TInt))

commutativityProof :: Maybe $ Dict (ArithRes Sub 'TNat 'TInt ~ ArithRes Sub 'TInt 'TNat, ArithOp Sub 'TInt 'TNat)

ArithOp Sub 'TNat 'TNat

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Sub 'TNat 'TNat :: T

Methods

convergeArith :: proxy Sub -> Notes 'TNat -> Notes 'TNat -> Either AnnConvergeError (Notes (ArithRes Sub 'TNat 'TNat))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Sub -> Value' instr 'TNat -> Value' instr 'TNat -> Either (ArithError (Value' instr 'TNat) (Value' instr 'TNat)) (Value' instr (ArithRes Sub 'TNat 'TNat))

commutativityProof :: Maybe $ Dict (ArithRes Sub 'TNat 'TNat ~ ArithRes Sub 'TNat 'TNat, ArithOp Sub 'TNat 'TNat)

ArithOp Sub 'TMutez 'TMutez

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Sub 'TMutez 'TMutez :: T

Methods

convergeArith :: proxy Sub -> Notes 'TMutez -> Notes 'TMutez -> Either AnnConvergeError (Notes (ArithRes Sub 'TMutez 'TMutez))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Sub -> Value' instr 'TMutez -> Value' instr 'TMutez -> Either (ArithError (Value' instr 'TMutez) (Value' instr 'TMutez)) (Value' instr (ArithRes Sub 'TMutez 'TMutez))

commutativityProof :: Maybe $ Dict (ArithRes Sub 'TMutez 'TMutez ~ ArithRes Sub 'TMutez 'TMutez, ArithOp Sub 'TMutez 'TMutez)

ArithOp Sub 'TTimestamp 'TInt

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Sub 'TTimestamp 'TInt :: T

Methods

convergeArith :: proxy Sub -> Notes 'TTimestamp -> Notes 'TInt -> Either AnnConvergeError (Notes (ArithRes Sub 'TTimestamp 'TInt))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Sub -> Value' instr 'TTimestamp -> Value' instr 'TInt -> Either (ArithError (Value' instr 'TTimestamp) (Value' instr 'TInt)) (Value' instr (ArithRes Sub 'TTimestamp 'TInt))

commutativityProof :: Maybe $ Dict (ArithRes Sub 'TTimestamp 'TInt ~ ArithRes Sub 'TInt 'TTimestamp, ArithOp Sub 'TInt 'TTimestamp)

ArithOp Sub 'TTimestamp 'TTimestamp

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Sub 'TTimestamp 'TTimestamp :: T

Methods

convergeArith :: proxy Sub -> Notes 'TTimestamp -> Notes 'TTimestamp -> Either AnnConvergeError (Notes (ArithRes Sub 'TTimestamp 'TTimestamp))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Sub -> Value' instr 'TTimestamp -> Value' instr 'TTimestamp -> Either (ArithError (Value' instr 'TTimestamp) (Value' instr 'TTimestamp)) (Value' instr (ArithRes Sub 'TTimestamp 'TTimestamp))

commutativityProof :: Maybe $ Dict (ArithRes Sub 'TTimestamp 'TTimestamp ~ ArithRes Sub 'TTimestamp 'TTimestamp, ArithOp Sub 'TTimestamp 'TTimestamp)

ArithOp Add 'TInt 'TInt

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Add 'TInt 'TInt :: T

Methods

convergeArith :: proxy Add -> Notes 'TInt -> Notes 'TInt -> Either AnnConvergeError (Notes (ArithRes Add 'TInt 'TInt))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Add -> Value' instr 'TInt -> Value' instr 'TInt -> Either (ArithError (Value' instr 'TInt) (Value' instr 'TInt)) (Value' instr (ArithRes Add 'TInt 'TInt))

commutativityProof :: Maybe $ Dict (ArithRes Add 'TInt 'TInt ~ ArithRes Add 'TInt 'TInt, ArithOp Add 'TInt 'TInt)

ArithOp Add 'TInt 'TNat

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Add 'TInt 'TNat :: T

Methods

convergeArith :: proxy Add -> Notes 'TInt -> Notes 'TNat -> Either AnnConvergeError (Notes (ArithRes Add 'TInt 'TNat))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Add -> Value' instr 'TInt -> Value' instr 'TNat -> Either (ArithError (Value' instr 'TInt) (Value' instr 'TNat)) (Value' instr (ArithRes Add 'TInt 'TNat))

commutativityProof :: Maybe $ Dict (ArithRes Add 'TInt 'TNat ~ ArithRes Add 'TNat 'TInt, ArithOp Add 'TNat 'TInt)

ArithOp Add 'TInt 'TTimestamp

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Add 'TInt 'TTimestamp :: T

Methods

convergeArith :: proxy Add -> Notes 'TInt -> Notes 'TTimestamp -> Either AnnConvergeError (Notes (ArithRes Add 'TInt 'TTimestamp))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Add -> Value' instr 'TInt -> Value' instr 'TTimestamp -> Either (ArithError (Value' instr 'TInt) (Value' instr 'TTimestamp)) (Value' instr (ArithRes Add 'TInt 'TTimestamp))

commutativityProof :: Maybe $ Dict (ArithRes Add 'TInt 'TTimestamp ~ ArithRes Add 'TTimestamp 'TInt, ArithOp Add 'TTimestamp 'TInt)

ArithOp Add 'TNat 'TInt

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Add 'TNat 'TInt :: T

Methods

convergeArith :: proxy Add -> Notes 'TNat -> Notes 'TInt -> Either AnnConvergeError (Notes (ArithRes Add 'TNat 'TInt))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Add -> Value' instr 'TNat -> Value' instr 'TInt -> Either (ArithError (Value' instr 'TNat) (Value' instr 'TInt)) (Value' instr (ArithRes Add 'TNat 'TInt))

commutativityProof :: Maybe $ Dict (ArithRes Add 'TNat 'TInt ~ ArithRes Add 'TInt 'TNat, ArithOp Add 'TInt 'TNat)

ArithOp Add 'TNat 'TNat

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Add 'TNat 'TNat :: T

Methods

convergeArith :: proxy Add -> Notes 'TNat -> Notes 'TNat -> Either AnnConvergeError (Notes (ArithRes Add 'TNat 'TNat))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Add -> Value' instr 'TNat -> Value' instr 'TNat -> Either (ArithError (Value' instr 'TNat) (Value' instr 'TNat)) (Value' instr (ArithRes Add 'TNat 'TNat))

commutativityProof :: Maybe $ Dict (ArithRes Add 'TNat 'TNat ~ ArithRes Add 'TNat 'TNat, ArithOp Add 'TNat 'TNat)

ArithOp Add 'TMutez 'TMutez

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Add 'TMutez 'TMutez :: T

Methods

convergeArith :: proxy Add -> Notes 'TMutez -> Notes 'TMutez -> Either AnnConvergeError (Notes (ArithRes Add 'TMutez 'TMutez))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Add -> Value' instr 'TMutez -> Value' instr 'TMutez -> Either (ArithError (Value' instr 'TMutez) (Value' instr 'TMutez)) (Value' instr (ArithRes Add 'TMutez 'TMutez))

commutativityProof :: Maybe $ Dict (ArithRes Add 'TMutez 'TMutez ~ ArithRes Add 'TMutez 'TMutez, ArithOp Add 'TMutez 'TMutez)

ArithOp Add 'TTimestamp 'TInt

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Add 'TTimestamp 'TInt :: T

Methods

convergeArith :: proxy Add -> Notes 'TTimestamp -> Notes 'TInt -> Either AnnConvergeError (Notes (ArithRes Add 'TTimestamp 'TInt))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Add -> Value' instr 'TTimestamp -> Value' instr 'TInt -> Either (ArithError (Value' instr 'TTimestamp) (Value' instr 'TInt)) (Value' instr (ArithRes Add 'TTimestamp 'TInt))

commutativityProof :: Maybe $ Dict (ArithRes Add 'TTimestamp 'TInt ~ ArithRes Add 'TInt 'TTimestamp, ArithOp Add 'TInt 'TTimestamp)

class UnaryArithOp aop (n :: T) where

Marker data type for add operation.

Associated Types

type UnaryArithRes aop n :: T

Methods

evalUnaryArithOp :: proxy aop -> Value' instr n -> Value' instr (UnaryArithRes aop n)

Instances

UnaryArithOp Ge 'TInt

Defined in Michelson.Typed.Arith

Associated Types

type UnaryArithRes Ge 'TInt :: T

Methods

evalUnaryArithOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Ge -> Value' instr 'TInt -> Value' instr (UnaryArithRes Ge 'TInt)

UnaryArithOp Le 'TInt

Defined in Michelson.Typed.Arith

Associated Types

type UnaryArithRes Le 'TInt :: T

Methods

evalUnaryArithOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Le -> Value' instr 'TInt -> Value' instr (UnaryArithRes Le 'TInt)

UnaryArithOp Gt 'TInt

Defined in Michelson.Typed.Arith

Associated Types

type UnaryArithRes Gt 'TInt :: T

Methods

evalUnaryArithOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Gt -> Value' instr 'TInt -> Value' instr (UnaryArithRes Gt 'TInt)

UnaryArithOp Lt 'TInt

Defined in Michelson.Typed.Arith

Associated Types

type UnaryArithRes Lt 'TInt :: T

Methods

evalUnaryArithOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Lt -> Value' instr 'TInt -> Value' instr (UnaryArithRes Lt 'TInt)

UnaryArithOp Neq 'TInt

Defined in Michelson.Typed.Arith

Associated Types

type UnaryArithRes Neq 'TInt :: T

Methods

evalUnaryArithOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Neq -> Value' instr 'TInt -> Value' instr (UnaryArithRes Neq 'TInt)

UnaryArithOp Eq' 'TInt

Defined in Michelson.Typed.Arith

Associated Types

type UnaryArithRes Eq' 'TInt :: T

Methods

evalUnaryArithOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Eq' -> Value' instr 'TInt -> Value' instr (UnaryArithRes Eq' 'TInt)

UnaryArithOp Not 'TInt

Defined in Michelson.Typed.Arith

Associated Types

type UnaryArithRes Not 'TInt :: T

Methods

evalUnaryArithOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Not -> Value' instr 'TInt -> Value' instr (UnaryArithRes Not 'TInt)

UnaryArithOp Not 'TNat

Defined in Michelson.Typed.Arith

Associated Types

type UnaryArithRes Not 'TNat :: T

Methods

evalUnaryArithOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Not -> Value' instr 'TNat -> Value' instr (UnaryArithRes Not 'TNat)

UnaryArithOp Not 'TBool

Defined in Michelson.Typed.Arith

Associated Types

type UnaryArithRes Not 'TBool :: T

Methods

evalUnaryArithOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Not -> Value' instr 'TBool -> Value' instr (UnaryArithRes Not 'TBool)

UnaryArithOp Neg 'TInt

Defined in Michelson.Typed.Arith

Associated Types

type UnaryArithRes Neg 'TInt :: T

Methods

evalUnaryArithOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Neg -> Value' instr 'TInt -> Value' instr (UnaryArithRes Neg 'TInt)

UnaryArithOp Neg 'TNat

Defined in Michelson.Typed.Arith

Associated Types

type UnaryArithRes Neg 'TNat :: T

Methods

evalUnaryArithOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Neg -> Value' instr 'TNat -> Value' instr (UnaryArithRes Neg 'TNat)

UnaryArithOp Abs 'TInt

Defined in Michelson.Typed.Arith

Associated Types

type UnaryArithRes Abs 'TInt :: T

Methods

evalUnaryArithOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Abs -> Value' instr 'TInt -> Value' instr (UnaryArithRes Abs 'TInt)

data ArithError n m

Represents an arithmetic error of the operation.

Constructors

MutezArithError MutezArithErrorType n m

ShiftArithError ShiftArithErrorType n m

Instances

(Eq n, Eq m) => Eq (ArithError n m)

Defined in Michelson.Typed.Arith

Methods

(==) :: ArithError n m -> ArithError n m -> Bool

(/=) :: ArithError n m -> ArithError n m -> Bool

(Ord n, Ord m) => Ord (ArithError n m)

Defined in Michelson.Typed.Arith

Methods

compare :: ArithError n m -> ArithError n m -> Ordering

(<) :: ArithError n m -> ArithError n m -> Bool

(<=) :: ArithError n m -> ArithError n m -> Bool

(>) :: ArithError n m -> ArithError n m -> Bool

(>=) :: ArithError n m -> ArithError n m -> Bool

max :: ArithError n m -> ArithError n m -> ArithError n m

min :: ArithError n m -> ArithError n m -> ArithError n m

(Show n, Show m) => Show (ArithError n m)

Defined in Michelson.Typed.Arith

Methods

showsPrec :: Int -> ArithError n m -> ShowS

show :: ArithError n m -> String

showList :: [ArithError n m] -> ShowS

Generic (ArithError n m)

Defined in Michelson.Typed.Arith

Associated Types

type Rep (ArithError n m) :: Type -> Type

Methods

from :: ArithError n m -> Rep (ArithError n m) x

to :: Rep (ArithError n m) x -> ArithError n m

(NFData n, NFData m) => NFData (ArithError n m)

Defined in Michelson.Typed.Arith

Methods

rnf :: ArithError n m -> ()

(Show n, Show m) => Buildable (ArithError n m)

Defined in Michelson.Typed.Arith

Methods

build :: ArithError n m -> Builder

type Rep (ArithError n m)

Defined in Michelson.Typed.Arith

type Rep (ArithError n m) = D1 ('MetaData "ArithError" "Michelson.Typed.Arith" "morley-1.10.0-inplace" 'False) (C1 ('MetaCons "MutezArithError" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 MutezArithErrorType) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 n) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 m))) :+: C1 ('MetaCons "ShiftArithError" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 ShiftArithErrorType) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 n) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 m))))

data ShiftArithErrorType

Denotes the error type occurred in the arithmetic shift operation.

Constructors

LslOverflow

LsrUnderflow

Instances

Eq ShiftArithErrorType

Defined in Michelson.Typed.Arith

Methods

(==) :: ShiftArithErrorType -> ShiftArithErrorType -> Bool

(/=) :: ShiftArithErrorType -> ShiftArithErrorType -> Bool

Ord ShiftArithErrorType

Defined in Michelson.Typed.Arith

Methods

compare :: ShiftArithErrorType -> ShiftArithErrorType -> Ordering

(<) :: ShiftArithErrorType -> ShiftArithErrorType -> Bool

(<=) :: ShiftArithErrorType -> ShiftArithErrorType -> Bool

(>) :: ShiftArithErrorType -> ShiftArithErrorType -> Bool

(>=) :: ShiftArithErrorType -> ShiftArithErrorType -> Bool

max :: ShiftArithErrorType -> ShiftArithErrorType -> ShiftArithErrorType

min :: ShiftArithErrorType -> ShiftArithErrorType -> ShiftArithErrorType

Show ShiftArithErrorType

Defined in Michelson.Typed.Arith

Methods

showsPrec :: Int -> ShiftArithErrorType -> ShowS

show :: ShiftArithErrorType -> String

showList :: [ShiftArithErrorType] -> ShowS

Generic ShiftArithErrorType

Defined in Michelson.Typed.Arith

Associated Types

type Rep ShiftArithErrorType :: Type -> Type

Methods

from :: ShiftArithErrorType -> Rep ShiftArithErrorType x

to :: Rep ShiftArithErrorType x -> ShiftArithErrorType

NFData ShiftArithErrorType

Defined in Michelson.Typed.Arith

Methods

rnf :: ShiftArithErrorType -> ()

Buildable ShiftArithErrorType

Defined in Michelson.Typed.Arith

Methods

build :: ShiftArithErrorType -> Builder

type Rep ShiftArithErrorType

Defined in Michelson.Typed.Arith

type Rep ShiftArithErrorType = D1 ('MetaData "ShiftArithErrorType" "Michelson.Typed.Arith" "morley-1.10.0-inplace" 'False) (C1 ('MetaCons "LslOverflow" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "LsrUnderflow" 'PrefixI 'False) (U1 :: Type -> Type))

data MutezArithErrorType

Denotes the error type occurred in the arithmetic operation involving mutez.

Constructors

AddOverflow

MulOverflow

SubUnderflow

Instances

Eq MutezArithErrorType

Defined in Michelson.Typed.Arith

Methods

(==) :: MutezArithErrorType -> MutezArithErrorType -> Bool

(/=) :: MutezArithErrorType -> MutezArithErrorType -> Bool

Ord MutezArithErrorType

Defined in Michelson.Typed.Arith

Methods

compare :: MutezArithErrorType -> MutezArithErrorType -> Ordering

(<) :: MutezArithErrorType -> MutezArithErrorType -> Bool

(<=) :: MutezArithErrorType -> MutezArithErrorType -> Bool

(>) :: MutezArithErrorType -> MutezArithErrorType -> Bool

(>=) :: MutezArithErrorType -> MutezArithErrorType -> Bool

max :: MutezArithErrorType -> MutezArithErrorType -> MutezArithErrorType

min :: MutezArithErrorType -> MutezArithErrorType -> MutezArithErrorType

Show MutezArithErrorType

Defined in Michelson.Typed.Arith

Methods

showsPrec :: Int -> MutezArithErrorType -> ShowS

show :: MutezArithErrorType -> String

showList :: [MutezArithErrorType] -> ShowS

Generic MutezArithErrorType

Defined in Michelson.Typed.Arith

Associated Types

type Rep MutezArithErrorType :: Type -> Type

Methods

from :: MutezArithErrorType -> Rep MutezArithErrorType x

to :: Rep MutezArithErrorType x -> MutezArithErrorType

NFData MutezArithErrorType

Defined in Michelson.Typed.Arith

Methods

rnf :: MutezArithErrorType -> ()

Buildable MutezArithErrorType

Defined in Michelson.Typed.Arith

Methods

build :: MutezArithErrorType -> Builder

type Rep MutezArithErrorType

Defined in Michelson.Typed.Arith

type Rep MutezArithErrorType = D1 ('MetaData "MutezArithErrorType" "Michelson.Typed.Arith" "morley-1.10.0-inplace" 'False) (C1 ('MetaCons "AddOverflow" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "MulOverflow" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SubUnderflow" 'PrefixI 'False) (U1 :: Type -> Type)))

data Add

Instances

ArithOp Add 'TInt 'TInt

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Add 'TInt 'TInt :: T

Methods

convergeArith :: proxy Add -> Notes 'TInt -> Notes 'TInt -> Either AnnConvergeError (Notes (ArithRes Add 'TInt 'TInt))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Add -> Value' instr 'TInt -> Value' instr 'TInt -> Either (ArithError (Value' instr 'TInt) (Value' instr 'TInt)) (Value' instr (ArithRes Add 'TInt 'TInt))

commutativityProof :: Maybe $ Dict (ArithRes Add 'TInt 'TInt ~ ArithRes Add 'TInt 'TInt, ArithOp Add 'TInt 'TInt)

ArithOp Add 'TInt 'TNat

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Add 'TInt 'TNat :: T

Methods

convergeArith :: proxy Add -> Notes 'TInt -> Notes 'TNat -> Either AnnConvergeError (Notes (ArithRes Add 'TInt 'TNat))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Add -> Value' instr 'TInt -> Value' instr 'TNat -> Either (ArithError (Value' instr 'TInt) (Value' instr 'TNat)) (Value' instr (ArithRes Add 'TInt 'TNat))

commutativityProof :: Maybe $ Dict (ArithRes Add 'TInt 'TNat ~ ArithRes Add 'TNat 'TInt, ArithOp Add 'TNat 'TInt)

ArithOp Add 'TInt 'TTimestamp

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Add 'TInt 'TTimestamp :: T

Methods

convergeArith :: proxy Add -> Notes 'TInt -> Notes 'TTimestamp -> Either AnnConvergeError (Notes (ArithRes Add 'TInt 'TTimestamp))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Add -> Value' instr 'TInt -> Value' instr 'TTimestamp -> Either (ArithError (Value' instr 'TInt) (Value' instr 'TTimestamp)) (Value' instr (ArithRes Add 'TInt 'TTimestamp))

commutativityProof :: Maybe $ Dict (ArithRes Add 'TInt 'TTimestamp ~ ArithRes Add 'TTimestamp 'TInt, ArithOp Add 'TTimestamp 'TInt)

ArithOp Add 'TNat 'TInt

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Add 'TNat 'TInt :: T

Methods

convergeArith :: proxy Add -> Notes 'TNat -> Notes 'TInt -> Either AnnConvergeError (Notes (ArithRes Add 'TNat 'TInt))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Add -> Value' instr 'TNat -> Value' instr 'TInt -> Either (ArithError (Value' instr 'TNat) (Value' instr 'TInt)) (Value' instr (ArithRes Add 'TNat 'TInt))

commutativityProof :: Maybe $ Dict (ArithRes Add 'TNat 'TInt ~ ArithRes Add 'TInt 'TNat, ArithOp Add 'TInt 'TNat)

ArithOp Add 'TNat 'TNat

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Add 'TNat 'TNat :: T

Methods

convergeArith :: proxy Add -> Notes 'TNat -> Notes 'TNat -> Either AnnConvergeError (Notes (ArithRes Add 'TNat 'TNat))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Add -> Value' instr 'TNat -> Value' instr 'TNat -> Either (ArithError (Value' instr 'TNat) (Value' instr 'TNat)) (Value' instr (ArithRes Add 'TNat 'TNat))

commutativityProof :: Maybe $ Dict (ArithRes Add 'TNat 'TNat ~ ArithRes Add 'TNat 'TNat, ArithOp Add 'TNat 'TNat)

ArithOp Add 'TMutez 'TMutez

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Add 'TMutez 'TMutez :: T

Methods

convergeArith :: proxy Add -> Notes 'TMutez -> Notes 'TMutez -> Either AnnConvergeError (Notes (ArithRes Add 'TMutez 'TMutez))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Add -> Value' instr 'TMutez -> Value' instr 'TMutez -> Either (ArithError (Value' instr 'TMutez) (Value' instr 'TMutez)) (Value' instr (ArithRes Add 'TMutez 'TMutez))

commutativityProof :: Maybe $ Dict (ArithRes Add 'TMutez 'TMutez ~ ArithRes Add 'TMutez 'TMutez, ArithOp Add 'TMutez 'TMutez)

ArithOp Add 'TTimestamp 'TInt

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Add 'TTimestamp 'TInt :: T

Methods

convergeArith :: proxy Add -> Notes 'TTimestamp -> Notes 'TInt -> Either AnnConvergeError (Notes (ArithRes Add 'TTimestamp 'TInt))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Add -> Value' instr 'TTimestamp -> Value' instr 'TInt -> Either (ArithError (Value' instr 'TTimestamp) (Value' instr 'TInt)) (Value' instr (ArithRes Add 'TTimestamp 'TInt))

commutativityProof :: Maybe $ Dict (ArithRes Add 'TTimestamp 'TInt ~ ArithRes Add 'TInt 'TTimestamp, ArithOp Add 'TInt 'TTimestamp)

type ArithRes Add 'TInt 'TInt

Defined in Michelson.Typed.Arith

type ArithRes Add 'TInt 'TInt = 'TInt

type ArithRes Add 'TInt 'TNat

Defined in Michelson.Typed.Arith

type ArithRes Add 'TInt 'TNat = 'TInt

type ArithRes Add 'TInt 'TTimestamp

Defined in Michelson.Typed.Arith

type ArithRes Add 'TInt 'TTimestamp = 'TTimestamp

type ArithRes Add 'TNat 'TInt

Defined in Michelson.Typed.Arith

type ArithRes Add 'TNat 'TInt = 'TInt

type ArithRes Add 'TNat 'TNat

Defined in Michelson.Typed.Arith

type ArithRes Add 'TNat 'TNat = 'TNat

type ArithRes Add 'TMutez 'TMutez

Defined in Michelson.Typed.Arith

type ArithRes Add 'TMutez 'TMutez = 'TMutez

type ArithRes Add 'TTimestamp 'TInt

Defined in Michelson.Typed.Arith

type ArithRes Add 'TTimestamp 'TInt = 'TTimestamp

data Sub

Instances

ArithOp Sub 'TInt 'TInt

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Sub 'TInt 'TInt :: T

Methods

convergeArith :: proxy Sub -> Notes 'TInt -> Notes 'TInt -> Either AnnConvergeError (Notes (ArithRes Sub 'TInt 'TInt))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Sub -> Value' instr 'TInt -> Value' instr 'TInt -> Either (ArithError (Value' instr 'TInt) (Value' instr 'TInt)) (Value' instr (ArithRes Sub 'TInt 'TInt))

commutativityProof :: Maybe $ Dict (ArithRes Sub 'TInt 'TInt ~ ArithRes Sub 'TInt 'TInt, ArithOp Sub 'TInt 'TInt)

ArithOp Sub 'TInt 'TNat

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Sub 'TInt 'TNat :: T

Methods

convergeArith :: proxy Sub -> Notes 'TInt -> Notes 'TNat -> Either AnnConvergeError (Notes (ArithRes Sub 'TInt 'TNat))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Sub -> Value' instr 'TInt -> Value' instr 'TNat -> Either (ArithError (Value' instr 'TInt) (Value' instr 'TNat)) (Value' instr (ArithRes Sub 'TInt 'TNat))

commutativityProof :: Maybe $ Dict (ArithRes Sub 'TInt 'TNat ~ ArithRes Sub 'TNat 'TInt, ArithOp Sub 'TNat 'TInt)

ArithOp Sub 'TNat 'TInt

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Sub 'TNat 'TInt :: T

Methods

convergeArith :: proxy Sub -> Notes 'TNat -> Notes 'TInt -> Either AnnConvergeError (Notes (ArithRes Sub 'TNat 'TInt))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Sub -> Value' instr 'TNat -> Value' instr 'TInt -> Either (ArithError (Value' instr 'TNat) (Value' instr 'TInt)) (Value' instr (ArithRes Sub 'TNat 'TInt))

commutativityProof :: Maybe $ Dict (ArithRes Sub 'TNat 'TInt ~ ArithRes Sub 'TInt 'TNat, ArithOp Sub 'TInt 'TNat)

ArithOp Sub 'TNat 'TNat

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Sub 'TNat 'TNat :: T

Methods

convergeArith :: proxy Sub -> Notes 'TNat -> Notes 'TNat -> Either AnnConvergeError (Notes (ArithRes Sub 'TNat 'TNat))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Sub -> Value' instr 'TNat -> Value' instr 'TNat -> Either (ArithError (Value' instr 'TNat) (Value' instr 'TNat)) (Value' instr (ArithRes Sub 'TNat 'TNat))

commutativityProof :: Maybe $ Dict (ArithRes Sub 'TNat 'TNat ~ ArithRes Sub 'TNat 'TNat, ArithOp Sub 'TNat 'TNat)

ArithOp Sub 'TMutez 'TMutez

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Sub 'TMutez 'TMutez :: T

Methods

convergeArith :: proxy Sub -> Notes 'TMutez -> Notes 'TMutez -> Either AnnConvergeError (Notes (ArithRes Sub 'TMutez 'TMutez))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Sub -> Value' instr 'TMutez -> Value' instr 'TMutez -> Either (ArithError (Value' instr 'TMutez) (Value' instr 'TMutez)) (Value' instr (ArithRes Sub 'TMutez 'TMutez))

commutativityProof :: Maybe $ Dict (ArithRes Sub 'TMutez 'TMutez ~ ArithRes Sub 'TMutez 'TMutez, ArithOp Sub 'TMutez 'TMutez)

ArithOp Sub 'TTimestamp 'TInt

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Sub 'TTimestamp 'TInt :: T

Methods

convergeArith :: proxy Sub -> Notes 'TTimestamp -> Notes 'TInt -> Either AnnConvergeError (Notes (ArithRes Sub 'TTimestamp 'TInt))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Sub -> Value' instr 'TTimestamp -> Value' instr 'TInt -> Either (ArithError (Value' instr 'TTimestamp) (Value' instr 'TInt)) (Value' instr (ArithRes Sub 'TTimestamp 'TInt))

commutativityProof :: Maybe $ Dict (ArithRes Sub 'TTimestamp 'TInt ~ ArithRes Sub 'TInt 'TTimestamp, ArithOp Sub 'TInt 'TTimestamp)

ArithOp Sub 'TTimestamp 'TTimestamp

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Sub 'TTimestamp 'TTimestamp :: T

Methods

convergeArith :: proxy Sub -> Notes 'TTimestamp -> Notes 'TTimestamp -> Either AnnConvergeError (Notes (ArithRes Sub 'TTimestamp 'TTimestamp))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Sub -> Value' instr 'TTimestamp -> Value' instr 'TTimestamp -> Either (ArithError (Value' instr 'TTimestamp) (Value' instr 'TTimestamp)) (Value' instr (ArithRes Sub 'TTimestamp 'TTimestamp))

commutativityProof :: Maybe $ Dict (ArithRes Sub 'TTimestamp 'TTimestamp ~ ArithRes Sub 'TTimestamp 'TTimestamp, ArithOp Sub 'TTimestamp 'TTimestamp)

type ArithRes Sub 'TInt 'TInt

Defined in Michelson.Typed.Arith

type ArithRes Sub 'TInt 'TInt = 'TInt

type ArithRes Sub 'TInt 'TNat

Defined in Michelson.Typed.Arith

type ArithRes Sub 'TInt 'TNat = 'TInt

type ArithRes Sub 'TNat 'TInt

Defined in Michelson.Typed.Arith

type ArithRes Sub 'TNat 'TInt = 'TInt

type ArithRes Sub 'TNat 'TNat

Defined in Michelson.Typed.Arith

type ArithRes Sub 'TNat 'TNat = 'TInt

type ArithRes Sub 'TMutez 'TMutez

Defined in Michelson.Typed.Arith

type ArithRes Sub 'TMutez 'TMutez = 'TMutez

type ArithRes Sub 'TTimestamp 'TInt

Defined in Michelson.Typed.Arith

type ArithRes Sub 'TTimestamp 'TInt = 'TTimestamp

type ArithRes Sub 'TTimestamp 'TTimestamp

Defined in Michelson.Typed.Arith

type ArithRes Sub 'TTimestamp 'TTimestamp = 'TInt

data Mul

Instances

ArithOp Mul 'TInt 'TInt

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Mul 'TInt 'TInt :: T

Methods

convergeArith :: proxy Mul -> Notes 'TInt -> Notes 'TInt -> Either AnnConvergeError (Notes (ArithRes Mul 'TInt 'TInt))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Mul -> Value' instr 'TInt -> Value' instr 'TInt -> Either (ArithError (Value' instr 'TInt) (Value' instr 'TInt)) (Value' instr (ArithRes Mul 'TInt 'TInt))

commutativityProof :: Maybe $ Dict (ArithRes Mul 'TInt 'TInt ~ ArithRes Mul 'TInt 'TInt, ArithOp Mul 'TInt 'TInt)

ArithOp Mul 'TInt 'TNat

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Mul 'TInt 'TNat :: T

Methods

convergeArith :: proxy Mul -> Notes 'TInt -> Notes 'TNat -> Either AnnConvergeError (Notes (ArithRes Mul 'TInt 'TNat))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Mul -> Value' instr 'TInt -> Value' instr 'TNat -> Either (ArithError (Value' instr 'TInt) (Value' instr 'TNat)) (Value' instr (ArithRes Mul 'TInt 'TNat))

commutativityProof :: Maybe $ Dict (ArithRes Mul 'TInt 'TNat ~ ArithRes Mul 'TNat 'TInt, ArithOp Mul 'TNat 'TInt)

ArithOp Mul 'TNat 'TInt

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Mul 'TNat 'TInt :: T

Methods

convergeArith :: proxy Mul -> Notes 'TNat -> Notes 'TInt -> Either AnnConvergeError (Notes (ArithRes Mul 'TNat 'TInt))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Mul -> Value' instr 'TNat -> Value' instr 'TInt -> Either (ArithError (Value' instr 'TNat) (Value' instr 'TInt)) (Value' instr (ArithRes Mul 'TNat 'TInt))

commutativityProof :: Maybe $ Dict (ArithRes Mul 'TNat 'TInt ~ ArithRes Mul 'TInt 'TNat, ArithOp Mul 'TInt 'TNat)

ArithOp Mul 'TNat 'TNat

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Mul 'TNat 'TNat :: T

Methods

convergeArith :: proxy Mul -> Notes 'TNat -> Notes 'TNat -> Either AnnConvergeError (Notes (ArithRes Mul 'TNat 'TNat))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Mul -> Value' instr 'TNat -> Value' instr 'TNat -> Either (ArithError (Value' instr 'TNat) (Value' instr 'TNat)) (Value' instr (ArithRes Mul 'TNat 'TNat))

commutativityProof :: Maybe $ Dict (ArithRes Mul 'TNat 'TNat ~ ArithRes Mul 'TNat 'TNat, ArithOp Mul 'TNat 'TNat)

ArithOp Mul 'TNat 'TMutez

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Mul 'TNat 'TMutez :: T

Methods

convergeArith :: proxy Mul -> Notes 'TNat -> Notes 'TMutez -> Either AnnConvergeError (Notes (ArithRes Mul 'TNat 'TMutez))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Mul -> Value' instr 'TNat -> Value' instr 'TMutez -> Either (ArithError (Value' instr 'TNat) (Value' instr 'TMutez)) (Value' instr (ArithRes Mul 'TNat 'TMutez))

commutativityProof :: Maybe $ Dict (ArithRes Mul 'TNat 'TMutez ~ ArithRes Mul 'TMutez 'TNat, ArithOp Mul 'TMutez 'TNat)

ArithOp Mul 'TMutez 'TNat

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Mul 'TMutez 'TNat :: T

Methods

convergeArith :: proxy Mul -> Notes 'TMutez -> Notes 'TNat -> Either AnnConvergeError (Notes (ArithRes Mul 'TMutez 'TNat))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Mul -> Value' instr 'TMutez -> Value' instr 'TNat -> Either (ArithError (Value' instr 'TMutez) (Value' instr 'TNat)) (Value' instr (ArithRes Mul 'TMutez 'TNat))

commutativityProof :: Maybe $ Dict (ArithRes Mul 'TMutez 'TNat ~ ArithRes Mul 'TNat 'TMutez, ArithOp Mul 'TNat 'TMutez)

type ArithRes Mul 'TInt 'TInt

Defined in Michelson.Typed.Arith

type ArithRes Mul 'TInt 'TInt = 'TInt

type ArithRes Mul 'TInt 'TNat

Defined in Michelson.Typed.Arith

type ArithRes Mul 'TInt 'TNat = 'TInt

type ArithRes Mul 'TNat 'TInt

Defined in Michelson.Typed.Arith

type ArithRes Mul 'TNat 'TInt = 'TInt

type ArithRes Mul 'TNat 'TNat

Defined in Michelson.Typed.Arith

type ArithRes Mul 'TNat 'TNat = 'TNat

type ArithRes Mul 'TNat 'TMutez

Defined in Michelson.Typed.Arith

type ArithRes Mul 'TNat 'TMutez = 'TMutez

type ArithRes Mul 'TMutez 'TNat

Defined in Michelson.Typed.Arith

type ArithRes Mul 'TMutez 'TNat = 'TMutez

data Abs

Instances

UnaryArithOp Abs 'TInt

Defined in Michelson.Typed.Arith

Associated Types

type UnaryArithRes Abs 'TInt :: T

Methods

evalUnaryArithOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Abs -> Value' instr 'TInt -> Value' instr (UnaryArithRes Abs 'TInt)

type UnaryArithRes Abs 'TInt

Defined in Michelson.Typed.Arith

type UnaryArithRes Abs 'TInt = 'TNat

data Neg

Instances

UnaryArithOp Neg 'TInt

Defined in Michelson.Typed.Arith

Associated Types

type UnaryArithRes Neg 'TInt :: T

Methods

evalUnaryArithOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Neg -> Value' instr 'TInt -> Value' instr (UnaryArithRes Neg 'TInt)

UnaryArithOp Neg 'TNat

Defined in Michelson.Typed.Arith

Associated Types

type UnaryArithRes Neg 'TNat :: T

Methods

evalUnaryArithOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Neg -> Value' instr 'TNat -> Value' instr (UnaryArithRes Neg 'TNat)

type UnaryArithRes Neg 'TInt

Defined in Michelson.Typed.Arith

type UnaryArithRes Neg 'TInt = 'TInt

type UnaryArithRes Neg 'TNat

Defined in Michelson.Typed.Arith

type UnaryArithRes Neg 'TNat = 'TInt

data Or

Instances

ArithOp Or 'TNat 'TNat

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Or 'TNat 'TNat :: T

Methods

convergeArith :: proxy Or -> Notes 'TNat -> Notes 'TNat -> Either AnnConvergeError (Notes (ArithRes Or 'TNat 'TNat))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Or -> Value' instr 'TNat -> Value' instr 'TNat -> Either (ArithError (Value' instr 'TNat) (Value' instr 'TNat)) (Value' instr (ArithRes Or 'TNat 'TNat))

commutativityProof :: Maybe $ Dict (ArithRes Or 'TNat 'TNat ~ ArithRes Or 'TNat 'TNat, ArithOp Or 'TNat 'TNat)

ArithOp Or 'TBool 'TBool

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Or 'TBool 'TBool :: T

Methods

convergeArith :: proxy Or -> Notes 'TBool -> Notes 'TBool -> Either AnnConvergeError (Notes (ArithRes Or 'TBool 'TBool))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Or -> Value' instr 'TBool -> Value' instr 'TBool -> Either (ArithError (Value' instr 'TBool) (Value' instr 'TBool)) (Value' instr (ArithRes Or 'TBool 'TBool))

commutativityProof :: Maybe $ Dict (ArithRes Or 'TBool 'TBool ~ ArithRes Or 'TBool 'TBool, ArithOp Or 'TBool 'TBool)

type ArithRes Or 'TNat 'TNat

Defined in Michelson.Typed.Arith

type ArithRes Or 'TNat 'TNat = 'TNat

type ArithRes Or 'TBool 'TBool

Defined in Michelson.Typed.Arith

type ArithRes Or 'TBool 'TBool = 'TBool

data And

Instances

ArithOp And 'TInt 'TNat

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes And 'TInt 'TNat :: T

Methods

convergeArith :: proxy And -> Notes 'TInt -> Notes 'TNat -> Either AnnConvergeError (Notes (ArithRes And 'TInt 'TNat))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy And -> Value' instr 'TInt -> Value' instr 'TNat -> Either (ArithError (Value' instr 'TInt) (Value' instr 'TNat)) (Value' instr (ArithRes And 'TInt 'TNat))

commutativityProof :: Maybe $ Dict (ArithRes And 'TInt 'TNat ~ ArithRes And 'TNat 'TInt, ArithOp And 'TNat 'TInt)

ArithOp And 'TNat 'TNat

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes And 'TNat 'TNat :: T

Methods

convergeArith :: proxy And -> Notes 'TNat -> Notes 'TNat -> Either AnnConvergeError (Notes (ArithRes And 'TNat 'TNat))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy And -> Value' instr 'TNat -> Value' instr 'TNat -> Either (ArithError (Value' instr 'TNat) (Value' instr 'TNat)) (Value' instr (ArithRes And 'TNat 'TNat))

commutativityProof :: Maybe $ Dict (ArithRes And 'TNat 'TNat ~ ArithRes And 'TNat 'TNat, ArithOp And 'TNat 'TNat)

ArithOp And 'TBool 'TBool

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes And 'TBool 'TBool :: T

Methods

convergeArith :: proxy And -> Notes 'TBool -> Notes 'TBool -> Either AnnConvergeError (Notes (ArithRes And 'TBool 'TBool))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy And -> Value' instr 'TBool -> Value' instr 'TBool -> Either (ArithError (Value' instr 'TBool) (Value' instr 'TBool)) (Value' instr (ArithRes And 'TBool 'TBool))

commutativityProof :: Maybe $ Dict (ArithRes And 'TBool 'TBool ~ ArithRes And 'TBool 'TBool, ArithOp And 'TBool 'TBool)

type ArithRes And 'TInt 'TNat

Defined in Michelson.Typed.Arith

type ArithRes And 'TInt 'TNat = 'TNat

type ArithRes And 'TNat 'TNat

Defined in Michelson.Typed.Arith

type ArithRes And 'TNat 'TNat = 'TNat

type ArithRes And 'TBool 'TBool

Defined in Michelson.Typed.Arith

type ArithRes And 'TBool 'TBool = 'TBool

data Xor

Instances

ArithOp Xor 'TNat 'TNat

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Xor 'TNat 'TNat :: T

Methods

convergeArith :: proxy Xor -> Notes 'TNat -> Notes 'TNat -> Either AnnConvergeError (Notes (ArithRes Xor 'TNat 'TNat))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Xor -> Value' instr 'TNat -> Value' instr 'TNat -> Either (ArithError (Value' instr 'TNat) (Value' instr 'TNat)) (Value' instr (ArithRes Xor 'TNat 'TNat))

commutativityProof :: Maybe $ Dict (ArithRes Xor 'TNat 'TNat ~ ArithRes Xor 'TNat 'TNat, ArithOp Xor 'TNat 'TNat)

ArithOp Xor 'TBool 'TBool

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Xor 'TBool 'TBool :: T

Methods

convergeArith :: proxy Xor -> Notes 'TBool -> Notes 'TBool -> Either AnnConvergeError (Notes (ArithRes Xor 'TBool 'TBool))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Xor -> Value' instr 'TBool -> Value' instr 'TBool -> Either (ArithError (Value' instr 'TBool) (Value' instr 'TBool)) (Value' instr (ArithRes Xor 'TBool 'TBool))

commutativityProof :: Maybe $ Dict (ArithRes Xor 'TBool 'TBool ~ ArithRes Xor 'TBool 'TBool, ArithOp Xor 'TBool 'TBool)

type ArithRes Xor 'TNat 'TNat

Defined in Michelson.Typed.Arith

type ArithRes Xor 'TNat 'TNat = 'TNat

type ArithRes Xor 'TBool 'TBool

Defined in Michelson.Typed.Arith

type ArithRes Xor 'TBool 'TBool = 'TBool

data Not

Instances

UnaryArithOp Not 'TInt

Defined in Michelson.Typed.Arith

Associated Types

type UnaryArithRes Not 'TInt :: T

Methods

evalUnaryArithOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Not -> Value' instr 'TInt -> Value' instr (UnaryArithRes Not 'TInt)

UnaryArithOp Not 'TNat

Defined in Michelson.Typed.Arith

Associated Types

type UnaryArithRes Not 'TNat :: T

Methods

evalUnaryArithOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Not -> Value' instr 'TNat -> Value' instr (UnaryArithRes Not 'TNat)

UnaryArithOp Not 'TBool

Defined in Michelson.Typed.Arith

Associated Types

type UnaryArithRes Not 'TBool :: T

Methods

evalUnaryArithOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Not -> Value' instr 'TBool -> Value' instr (UnaryArithRes Not 'TBool)

type UnaryArithRes Not 'TInt

Defined in Michelson.Typed.Arith

type UnaryArithRes Not 'TInt = 'TInt

type UnaryArithRes Not 'TNat

Defined in Michelson.Typed.Arith

type UnaryArithRes Not 'TNat = 'TInt

type UnaryArithRes Not 'TBool

Defined in Michelson.Typed.Arith

type UnaryArithRes Not 'TBool = 'TBool

data Lsl

Instances

ArithOp Lsl 'TNat 'TNat

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Lsl 'TNat 'TNat :: T

Methods

convergeArith :: proxy Lsl -> Notes 'TNat -> Notes 'TNat -> Either AnnConvergeError (Notes (ArithRes Lsl 'TNat 'TNat))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Lsl -> Value' instr 'TNat -> Value' instr 'TNat -> Either (ArithError (Value' instr 'TNat) (Value' instr 'TNat)) (Value' instr (ArithRes Lsl 'TNat 'TNat))

commutativityProof :: Maybe $ Dict (ArithRes Lsl 'TNat 'TNat ~ ArithRes Lsl 'TNat 'TNat, ArithOp Lsl 'TNat 'TNat)

type ArithRes Lsl 'TNat 'TNat

Defined in Michelson.Typed.Arith

type ArithRes Lsl 'TNat 'TNat = 'TNat

data Lsr

Instances

ArithOp Lsr 'TNat 'TNat

Defined in Michelson.Typed.Arith

Associated Types

type ArithRes Lsr 'TNat 'TNat :: T

Methods

convergeArith :: proxy Lsr -> Notes 'TNat -> Notes 'TNat -> Either AnnConvergeError (Notes (ArithRes Lsr 'TNat 'TNat))

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Lsr -> Value' instr 'TNat -> Value' instr 'TNat -> Either (ArithError (Value' instr 'TNat) (Value' instr 'TNat)) (Value' instr (ArithRes Lsr 'TNat 'TNat))

commutativityProof :: Maybe $ Dict (ArithRes Lsr 'TNat 'TNat ~ ArithRes Lsr 'TNat 'TNat, ArithOp Lsr 'TNat 'TNat)

type ArithRes Lsr 'TNat 'TNat

Defined in Michelson.Typed.Arith

type ArithRes Lsr 'TNat 'TNat = 'TNat

data Compare

data Eq'

Instances

UnaryArithOp Eq' 'TInt

Defined in Michelson.Typed.Arith

Associated Types

type UnaryArithRes Eq' 'TInt :: T

Methods

evalUnaryArithOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Eq' -> Value' instr 'TInt -> Value' instr (UnaryArithRes Eq' 'TInt)

type UnaryArithRes Eq' 'TInt

Defined in Michelson.Typed.Arith

type UnaryArithRes Eq' 'TInt = 'TBool

data Neq

Instances

UnaryArithOp Neq 'TInt

Defined in Michelson.Typed.Arith

Associated Types

type UnaryArithRes Neq 'TInt :: T

Methods

evalUnaryArithOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Neq -> Value' instr 'TInt -> Value' instr (UnaryArithRes Neq 'TInt)

type UnaryArithRes Neq 'TInt

Defined in Michelson.Typed.Arith

type UnaryArithRes Neq 'TInt = 'TBool

data Lt

Instances

UnaryArithOp Lt 'TInt

Defined in Michelson.Typed.Arith

Associated Types

type UnaryArithRes Lt 'TInt :: T

Methods

evalUnaryArithOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Lt -> Value' instr 'TInt -> Value' instr (UnaryArithRes Lt 'TInt)

type UnaryArithRes Lt 'TInt

Defined in Michelson.Typed.Arith

type UnaryArithRes Lt 'TInt = 'TBool

data Gt

Instances

UnaryArithOp Gt 'TInt

Defined in Michelson.Typed.Arith

Associated Types

type UnaryArithRes Gt 'TInt :: T

Methods

evalUnaryArithOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Gt -> Value' instr 'TInt -> Value' instr (UnaryArithRes Gt 'TInt)

type UnaryArithRes Gt 'TInt

Defined in Michelson.Typed.Arith

type UnaryArithRes Gt 'TInt = 'TBool

data Le

Instances

UnaryArithOp Le 'TInt

Defined in Michelson.Typed.Arith

Associated Types

type UnaryArithRes Le 'TInt :: T

Methods

evalUnaryArithOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Le -> Value' instr 'TInt -> Value' instr (UnaryArithRes Le 'TInt)

type UnaryArithRes Le 'TInt

Defined in Michelson.Typed.Arith

type UnaryArithRes Le 'TInt = 'TBool

data Ge

Instances

UnaryArithOp Ge 'TInt

Defined in Michelson.Typed.Arith

Associated Types

type UnaryArithRes Ge 'TInt :: T

Methods

evalUnaryArithOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Ge -> Value' instr 'TInt -> Value' instr (UnaryArithRes Ge 'TInt)

type UnaryArithRes Ge 'TInt

Defined in Michelson.Typed.Arith

type UnaryArithRes Ge 'TInt = 'TBool

compareOp :: forall t i. (Comparable t, SingI t) => Value' i t -> Value' i t -> Integer