Lorentz.Arith

Type families from Morley.Michelson.Typed.Arith lifted to Haskell types.

Documentation

class ArithOpHs (aop :: Type) (n :: Type) (m :: Type) (r :: Type) where

Lifted ArithOp.

Minimal complete definition

Nothing

Methods

evalArithOpHs :: (n ': (m ': s)) :-> (r ': s)

default evalArithOpHs :: (DefArithOp aop, ArithOp aop (ToT n) (ToT m), ToT r ~ ArithRes aop (ToT n) (ToT m)) => (n ': (m ': s)) :-> (r ': s)

Instances

r ~ Integer => ArithOpHs Add Integer Integer r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Integer ': (Integer ': s)) :-> (r ': s)

r ~ Integer => ArithOpHs Add Integer Natural r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Integer ': (Natural ': s)) :-> (r ': s)

r ~ Timestamp => ArithOpHs Add Integer Timestamp r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Integer ': (Timestamp ': s)) :-> (r ': s)

r ~ Integer => ArithOpHs Add Natural Integer r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Natural ': (Integer ': s)) :-> (r ': s)

r ~ Natural => ArithOpHs Add Natural Natural r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Natural ': (Natural ': s)) :-> (r ': s)

r ~ Bls12381Fr => ArithOpHs Add Bls12381Fr Bls12381Fr r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Bls12381Fr ': (Bls12381Fr ': s)) :-> (r ': s)

r ~ Bls12381G1 => ArithOpHs Add Bls12381G1 Bls12381G1 r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Bls12381G1 ': (Bls12381G1 ': s)) :-> (r ': s)

r ~ Bls12381G2 => ArithOpHs Add Bls12381G2 Bls12381G2 r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Bls12381G2 ': (Bls12381G2 ': s)) :-> (r ': s)

r ~ Mutez => ArithOpHs Add Mutez Mutez r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Mutez ': (Mutez ': s)) :-> (r ': s)

r ~ Timestamp => ArithOpHs Add Timestamp Integer r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Timestamp ': (Integer ': s)) :-> (r ': s)

r ~ Bool => ArithOpHs And Bool Bool r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Bool ': (Bool ': s)) :-> (r ': s)

r ~ Natural => ArithOpHs And Integer Natural r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Integer ': (Natural ': s)) :-> (r ': s)

r ~ Natural => ArithOpHs And Natural Natural r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Natural ': (Natural ': s)) :-> (r ': s)

r ~ Maybe (Integer, Natural) => ArithOpHs EDiv Integer Integer r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Integer ': (Integer ': s)) :-> (r ': s)

r ~ Maybe (Integer, Natural) => ArithOpHs EDiv Integer Natural r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Integer ': (Natural ': s)) :-> (r ': s)

r ~ Maybe (Integer, Natural) => ArithOpHs EDiv Natural Integer r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Natural ': (Integer ': s)) :-> (r ': s)

r ~ Maybe (Natural, Natural) => ArithOpHs EDiv Natural Natural r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Natural ': (Natural ': s)) :-> (r ': s)

r ~ Maybe (Mutez, Mutez) => ArithOpHs EDiv Mutez Natural r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Mutez ': (Natural ': s)) :-> (r ': s)

r ~ Maybe (Natural, Mutez) => ArithOpHs EDiv Mutez Mutez r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Mutez ': (Mutez ': s)) :-> (r ': s)

r ~ Natural => ArithOpHs Lsl Natural Natural r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Natural ': (Natural ': s)) :-> (r ': s)

r ~ Natural => ArithOpHs Lsr Natural Natural r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Natural ': (Natural ': s)) :-> (r ': s)

r ~ Integer => ArithOpHs Mul Integer Integer r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Integer ': (Integer ': s)) :-> (r ': s)

r ~ Integer => ArithOpHs Mul Integer Natural r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Integer ': (Natural ': s)) :-> (r ': s)

r ~ Bls12381Fr => ArithOpHs Mul Integer Bls12381Fr r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Integer ': (Bls12381Fr ': s)) :-> (r ': s)

r ~ Integer => ArithOpHs Mul Natural Integer r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Natural ': (Integer ': s)) :-> (r ': s)

r ~ Natural => ArithOpHs Mul Natural Natural r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Natural ': (Natural ': s)) :-> (r ': s)

r ~ Bls12381Fr => ArithOpHs Mul Natural Bls12381Fr r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Natural ': (Bls12381Fr ': s)) :-> (r ': s)

r ~ Mutez => ArithOpHs Mul Natural Mutez r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Natural ': (Mutez ': s)) :-> (r ': s)

r ~ Bls12381Fr => ArithOpHs Mul Bls12381Fr Integer r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Bls12381Fr ': (Integer ': s)) :-> (r ': s)

r ~ Bls12381Fr => ArithOpHs Mul Bls12381Fr Natural r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Bls12381Fr ': (Natural ': s)) :-> (r ': s)

r ~ Bls12381Fr => ArithOpHs Mul Bls12381Fr Bls12381Fr r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Bls12381Fr ': (Bls12381Fr ': s)) :-> (r ': s)

r ~ Bls12381G1 => ArithOpHs Mul Bls12381Fr Bls12381G1 r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Bls12381Fr ': (Bls12381G1 ': s)) :-> (r ': s)

r ~ Bls12381G2 => ArithOpHs Mul Bls12381Fr Bls12381G2 r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Bls12381Fr ': (Bls12381G2 ': s)) :-> (r ': s)

r ~ Bls12381G1 => ArithOpHs Mul Bls12381G1 Bls12381Fr r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Bls12381G1 ': (Bls12381Fr ': s)) :-> (r ': s)

r ~ Bls12381G2 => ArithOpHs Mul Bls12381G2 Bls12381Fr r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Bls12381G2 ': (Bls12381Fr ': s)) :-> (r ': s)

r ~ Mutez => ArithOpHs Mul Mutez Natural r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Mutez ': (Natural ': s)) :-> (r ': s)

r ~ Bool => ArithOpHs Or Bool Bool r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Bool ': (Bool ': s)) :-> (r ': s)

r ~ Natural => ArithOpHs Or Natural Natural r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Natural ': (Natural ': s)) :-> (r ': s)

r ~ Integer => ArithOpHs Sub Integer Integer r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Integer ': (Integer ': s)) :-> (r ': s)

r ~ Integer => ArithOpHs Sub Integer Natural r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Integer ': (Natural ': s)) :-> (r ': s)

r ~ Integer => ArithOpHs Sub Natural Integer r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Natural ': (Integer ': s)) :-> (r ': s)

r ~ Integer => ArithOpHs Sub Natural Natural r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Natural ': (Natural ': s)) :-> (r ': s)

r ~ Mutez => ArithOpHs Sub Mutez Mutez r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Mutez ': (Mutez ': s)) :-> (r ': s)

r ~ Timestamp => ArithOpHs Sub Timestamp Integer r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Timestamp ': (Integer ': s)) :-> (r ': s)

r ~ Integer => ArithOpHs Sub Timestamp Timestamp r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Timestamp ': (Timestamp ': s)) :-> (r ': s)

r ~ Bool => ArithOpHs Xor Bool Bool r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Bool ': (Bool ': s)) :-> (r ': s)

r ~ Natural => ArithOpHs Xor Natural Natural r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Natural ': (Natural ': s)) :-> (r ': s)

r ~ Fixed p => ArithOpHs Add Integer (Fixed p) r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Integer ': (Fixed p ': s)) :-> (r ': s)

r ~ Fixed p => ArithOpHs Add Integer (NFixed p) r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Integer ': (NFixed p ': s)) :-> (r ': s)

r ~ Fixed p => ArithOpHs Add Natural (Fixed p) r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Natural ': (Fixed p ': s)) :-> (r ': s)

r ~ NFixed p => ArithOpHs Add Natural (NFixed p) r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Natural ': (NFixed p ': s)) :-> (r ': s)

r ~ Fixed p => ArithOpHs Mul Integer (Fixed p) r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Integer ': (Fixed p ': s)) :-> (r ': s)

r ~ Fixed p => ArithOpHs Mul Integer (NFixed p) r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Integer ': (NFixed p ': s)) :-> (r ': s)

r ~ Fixed p => ArithOpHs Mul Natural (Fixed p) r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Natural ': (Fixed p ': s)) :-> (r ': s)

r ~ NFixed p => ArithOpHs Mul Natural (NFixed p) r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Natural ': (NFixed p ': s)) :-> (r ': s)

r ~ Fixed p => ArithOpHs Sub Integer (Fixed p) r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Integer ': (Fixed p ': s)) :-> (r ': s)

r ~ Fixed p => ArithOpHs Sub Integer (NFixed p) r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Integer ': (NFixed p ': s)) :-> (r ': s)

r ~ Fixed p => ArithOpHs Sub Natural (Fixed p) r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Natural ': (Fixed p ': s)) :-> (r ': s)

r ~ Fixed p => ArithOpHs Sub Natural (NFixed p) r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Natural ': (NFixed p ': s)) :-> (r ': s)

r ~ Fixed p => ArithOpHs Add (Fixed p) Natural r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Fixed p ': (Natural ': s)) :-> (r ': s)

r ~ Fixed p => ArithOpHs Add (Fixed p) Integer r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Fixed p ': (Integer ': s)) :-> (r ': s)

r ~ NFixed p => ArithOpHs Add (NFixed p) Natural r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (NFixed p ': (Natural ': s)) :-> (r ': s)

r ~ Fixed p => ArithOpHs Add (NFixed p) Integer r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (NFixed p ': (Integer ': s)) :-> (r ': s)

(r ~ Maybe (Integer, NFixed (BinBase a)), KnownNat a) => ArithOpHs EDiv (Fixed (BinBase a)) Natural r

Defined in Lorentz.FixedArith

Methods

evalArithOpHs :: forall (s :: [Type]). (Fixed (BinBase a) ': (Natural ': s)) :-> (r ': s)

(r ~ Maybe (Integer, NFixed (BinBase a)), KnownNat a) => ArithOpHs EDiv (Fixed (BinBase a)) Integer r

Defined in Lorentz.FixedArith

Methods

evalArithOpHs :: forall (s :: [Type]). (Fixed (BinBase a) ': (Integer ': s)) :-> (r ': s)

(r ~ Maybe (Integer, NFixed (DecBase a)), KnownNat a) => ArithOpHs EDiv (Fixed (DecBase a)) Natural r

Defined in Lorentz.FixedArith

Methods

evalArithOpHs :: forall (s :: [Type]). (Fixed (DecBase a) ': (Natural ': s)) :-> (r ': s)

(r ~ Maybe (Integer, NFixed (DecBase a)), KnownNat a) => ArithOpHs EDiv (Fixed (DecBase a)) Integer r

Defined in Lorentz.FixedArith

Methods

evalArithOpHs :: forall (s :: [Type]). (Fixed (DecBase a) ': (Integer ': s)) :-> (r ': s)

(r ~ Maybe (Natural, NFixed (BinBase a)), KnownNat a) => ArithOpHs EDiv (NFixed (BinBase a)) Natural r

Defined in Lorentz.FixedArith

Methods

evalArithOpHs :: forall (s :: [Type]). (NFixed (BinBase a) ': (Natural ': s)) :-> (r ': s)

(r ~ Maybe (Integer, NFixed (BinBase a)), KnownNat a) => ArithOpHs EDiv (NFixed (BinBase a)) Integer r

Defined in Lorentz.FixedArith

Methods

evalArithOpHs :: forall (s :: [Type]). (NFixed (BinBase a) ': (Integer ': s)) :-> (r ': s)

(r ~ Maybe (Natural, NFixed (DecBase a)), KnownNat a) => ArithOpHs EDiv (NFixed (DecBase a)) Natural r

Defined in Lorentz.FixedArith

Methods

evalArithOpHs :: forall (s :: [Type]). (NFixed (DecBase a) ': (Natural ': s)) :-> (r ': s)

(r ~ Maybe (Integer, NFixed (DecBase a)), KnownNat a) => ArithOpHs EDiv (NFixed (DecBase a)) Integer r

Defined in Lorentz.FixedArith

Methods

evalArithOpHs :: forall (s :: [Type]). (NFixed (DecBase a) ': (Integer ': s)) :-> (r ': s)

r ~ NFixed (BinBase b) => ArithOpHs Lsl (NFixed (BinBase a)) Natural r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (NFixed (BinBase a) ': (Natural ': s)) :-> (r ': s)

r ~ NFixed (BinBase b) => ArithOpHs Lsr (NFixed (BinBase a)) Natural r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (NFixed (BinBase a) ': (Natural ': s)) :-> (r ': s)

r ~ Fixed p => ArithOpHs Mul (Fixed p) Natural r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Fixed p ': (Natural ': s)) :-> (r ': s)

r ~ Fixed p => ArithOpHs Mul (Fixed p) Integer r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Fixed p ': (Integer ': s)) :-> (r ': s)

r ~ NFixed p => ArithOpHs Mul (NFixed p) Natural r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (NFixed p ': (Natural ': s)) :-> (r ': s)

r ~ Fixed p => ArithOpHs Mul (NFixed p) Integer r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (NFixed p ': (Integer ': s)) :-> (r ': s)

r ~ Fixed p => ArithOpHs Sub (Fixed p) Natural r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Fixed p ': (Natural ': s)) :-> (r ': s)

r ~ Fixed p => ArithOpHs Sub (Fixed p) Integer r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Fixed p ': (Integer ': s)) :-> (r ': s)

r ~ Fixed p => ArithOpHs Sub (NFixed p) Natural r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (NFixed p ': (Natural ': s)) :-> (r ': s)

r ~ Fixed p => ArithOpHs Sub (NFixed p) Integer r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (NFixed p ': (Integer ': s)) :-> (r ': s)

r ~ Fixed p => ArithOpHs Add (Fixed p) (NFixed p) r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Fixed p ': (NFixed p ': s)) :-> (r ': s)

r ~ Fixed p => ArithOpHs Add (Fixed p) (Fixed p) r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Fixed p ': (Fixed p ': s)) :-> (r ': s)

r ~ Fixed p => ArithOpHs Add (NFixed p) (Fixed p) r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (NFixed p ': (Fixed p ': s)) :-> (r ': s)

r ~ NFixed p => ArithOpHs Add (NFixed p) (NFixed p) r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (NFixed p ': (NFixed p ': s)) :-> (r ': s)

r ~ Fixed p => ArithOpHs Sub (Fixed p) (NFixed p) r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Fixed p ': (NFixed p ': s)) :-> (r ': s)

r ~ Fixed p => ArithOpHs Sub (Fixed p) (Fixed p) r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Fixed p ': (Fixed p ': s)) :-> (r ': s)

r ~ Fixed p => ArithOpHs Sub (NFixed p) (Fixed p) r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (NFixed p ': (Fixed p ': s)) :-> (r ': s)

r ~ Fixed p => ArithOpHs Sub (NFixed p) (NFixed p) r

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (NFixed p ': (NFixed p ': s)) :-> (r ': s)

r ~ (a + b) => ArithOpHs Mul (Fixed (BinBase a)) (NFixed (BinBase b)) (Fixed (BinBase r))

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Fixed (BinBase a) ': (NFixed (BinBase b) ': s)) :-> (Fixed (BinBase r) ': s)

r ~ (a + b) => ArithOpHs Mul (Fixed (BinBase a)) (Fixed (BinBase b)) (Fixed (BinBase r))

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Fixed (BinBase a) ': (Fixed (BinBase b) ': s)) :-> (Fixed (BinBase r) ': s)

r ~ (a + b) => ArithOpHs Mul (Fixed (DecBase a)) (NFixed (DecBase b)) (Fixed (DecBase r))

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Fixed (DecBase a) ': (NFixed (DecBase b) ': s)) :-> (Fixed (DecBase r) ': s)

r ~ (a + b) => ArithOpHs Mul (Fixed (DecBase a)) (Fixed (DecBase b)) (Fixed (DecBase r))

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (Fixed (DecBase a) ': (Fixed (DecBase b) ': s)) :-> (Fixed (DecBase r) ': s)

r ~ (a + b) => ArithOpHs Mul (NFixed (BinBase a)) (Fixed (BinBase b)) (Fixed (BinBase r))

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (NFixed (BinBase a) ': (Fixed (BinBase b) ': s)) :-> (Fixed (BinBase r) ': s)

r ~ (a + b) => ArithOpHs Mul (NFixed (BinBase a)) (NFixed (BinBase b)) (NFixed (BinBase r))

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (NFixed (BinBase a) ': (NFixed (BinBase b) ': s)) :-> (NFixed (BinBase r) ': s)

r ~ (a + b) => ArithOpHs Mul (NFixed (DecBase a)) (Fixed (DecBase b)) (Fixed (DecBase r))

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (NFixed (DecBase a) ': (Fixed (DecBase b) ': s)) :-> (Fixed (DecBase r) ': s)

r ~ (a + b) => ArithOpHs Mul (NFixed (DecBase a)) (NFixed (DecBase b)) (NFixed (DecBase r))

Defined in Lorentz.Arith

Methods

evalArithOpHs :: forall (s :: [Type]). (NFixed (DecBase a) ': (NFixed (DecBase b) ': s)) :-> (NFixed (DecBase r) ': s)

class DefArithOp aop where

Helper typeclass that provides default definition of evalArithOpHs.

Methods

defEvalOpHs :: (ArithOp aop n m, r ~ ArithRes aop n m) => Instr (n ': (m ': s)) (r ': s)

Instances

DefArithOp Add

Defined in Lorentz.Arith

Methods

defEvalOpHs :: forall (n :: T) (m :: T) (r :: T) (s :: [T]). (ArithOp Add n m, r ~ ArithRes Add n m) => Instr (n ': (m ': s)) (r ': s)

DefArithOp And

Defined in Lorentz.Arith

Methods

defEvalOpHs :: forall (n :: T) (m :: T) (r :: T) (s :: [T]). (ArithOp And n m, r ~ ArithRes And n m) => Instr (n ': (m ': s)) (r ': s)

DefArithOp EDiv

Defined in Lorentz.Arith

Methods

defEvalOpHs :: forall (n :: T) (m :: T) (r :: T) (s :: [T]). (ArithOp EDiv n m, r ~ ArithRes EDiv n m) => Instr (n ': (m ': s)) (r ': s)

DefArithOp Lsl

Defined in Lorentz.Arith

Methods

defEvalOpHs :: forall (n :: T) (m :: T) (r :: T) (s :: [T]). (ArithOp Lsl n m, r ~ ArithRes Lsl n m) => Instr (n ': (m ': s)) (r ': s)

DefArithOp Lsr

Defined in Lorentz.Arith

Methods

defEvalOpHs :: forall (n :: T) (m :: T) (r :: T) (s :: [T]). (ArithOp Lsr n m, r ~ ArithRes Lsr n m) => Instr (n ': (m ': s)) (r ': s)

DefArithOp Mul

Defined in Lorentz.Arith

Methods

defEvalOpHs :: forall (n :: T) (m :: T) (r :: T) (s :: [T]). (ArithOp Mul n m, r ~ ArithRes Mul n m) => Instr (n ': (m ': s)) (r ': s)

DefArithOp Or

Defined in Lorentz.Arith

Methods

defEvalOpHs :: forall (n :: T) (m :: T) (r :: T) (s :: [T]). (ArithOp Or n m, r ~ ArithRes Or n m) => Instr (n ': (m ': s)) (r ': s)

DefArithOp Sub

Defined in Lorentz.Arith

Methods

defEvalOpHs :: forall (n :: T) (m :: T) (r :: T) (s :: [T]). (ArithOp Sub n m, r ~ ArithRes Sub n m) => Instr (n ': (m ': s)) (r ': s)

DefArithOp Xor

Defined in Lorentz.Arith

Methods

defEvalOpHs :: forall (n :: T) (m :: T) (r :: T) (s :: [T]). (ArithOp Xor n m, r ~ ArithRes Xor n m) => Instr (n ': (m ': s)) (r ': s)

class UnaryArithOpHs (aop :: Type) (n :: Type) where

Lifted UnaryArithOp.

Minimal complete definition

Nothing

Associated Types

type UnaryArithResHs aop n :: Type

Methods

evalUnaryArithOpHs :: (n ': s) :-> (UnaryArithResHs aop n ': s)

default evalUnaryArithOpHs :: (DefUnaryArithOp aop, UnaryArithOp aop (ToT n), ToT (UnaryArithResHs aop n) ~ UnaryArithRes aop (ToT n)) => (n ': s) :-> (UnaryArithResHs aop n ': s)

Instances

UnaryArithOpHs Abs Integer

Defined in Lorentz.Arith

Associated Types

type UnaryArithResHs Abs Integer

Methods

evalUnaryArithOpHs :: forall (s :: [Type]). (Integer ': s) :-> (UnaryArithResHs Abs Integer ': s)

UnaryArithOpHs Eq' Integer

Defined in Lorentz.Arith

Associated Types

type UnaryArithResHs Eq' Integer

Methods

evalUnaryArithOpHs :: forall (s :: [Type]). (Integer ': s) :-> (UnaryArithResHs Eq' Integer ': s)

UnaryArithOpHs Eq' Natural

Defined in Lorentz.Arith

Associated Types

type UnaryArithResHs Eq' Natural

Methods

evalUnaryArithOpHs :: forall (s :: [Type]). (Natural ': s) :-> (UnaryArithResHs Eq' Natural ': s)

UnaryArithOpHs Ge Integer

Defined in Lorentz.Arith

Associated Types

type UnaryArithResHs Ge Integer

Methods

evalUnaryArithOpHs :: forall (s :: [Type]). (Integer ': s) :-> (UnaryArithResHs Ge Integer ': s)

UnaryArithOpHs Ge Natural

Defined in Lorentz.Arith

Associated Types

type UnaryArithResHs Ge Natural

Methods

evalUnaryArithOpHs :: forall (s :: [Type]). (Natural ': s) :-> (UnaryArithResHs Ge Natural ': s)

UnaryArithOpHs Gt Integer

Defined in Lorentz.Arith

Associated Types

type UnaryArithResHs Gt Integer

Methods

evalUnaryArithOpHs :: forall (s :: [Type]). (Integer ': s) :-> (UnaryArithResHs Gt Integer ': s)

UnaryArithOpHs Gt Natural

Defined in Lorentz.Arith

Associated Types

type UnaryArithResHs Gt Natural

Methods

evalUnaryArithOpHs :: forall (s :: [Type]). (Natural ': s) :-> (UnaryArithResHs Gt Natural ': s)

UnaryArithOpHs Le Integer

Defined in Lorentz.Arith

Associated Types

type UnaryArithResHs Le Integer

Methods

evalUnaryArithOpHs :: forall (s :: [Type]). (Integer ': s) :-> (UnaryArithResHs Le Integer ': s)

UnaryArithOpHs Le Natural

Defined in Lorentz.Arith

Associated Types

type UnaryArithResHs Le Natural

Methods

evalUnaryArithOpHs :: forall (s :: [Type]). (Natural ': s) :-> (UnaryArithResHs Le Natural ': s)

UnaryArithOpHs Lt Integer

Defined in Lorentz.Arith

Associated Types

type UnaryArithResHs Lt Integer

Methods

evalUnaryArithOpHs :: forall (s :: [Type]). (Integer ': s) :-> (UnaryArithResHs Lt Integer ': s)

UnaryArithOpHs Lt Natural

Defined in Lorentz.Arith

Associated Types

type UnaryArithResHs Lt Natural

Methods

evalUnaryArithOpHs :: forall (s :: [Type]). (Natural ': s) :-> (UnaryArithResHs Lt Natural ': s)

UnaryArithOpHs Neg Integer

Defined in Lorentz.Arith

Associated Types

type UnaryArithResHs Neg Integer

Methods

evalUnaryArithOpHs :: forall (s :: [Type]). (Integer ': s) :-> (UnaryArithResHs Neg Integer ': s)

UnaryArithOpHs Neg Natural

Defined in Lorentz.Arith

Associated Types

type UnaryArithResHs Neg Natural

Methods

evalUnaryArithOpHs :: forall (s :: [Type]). (Natural ': s) :-> (UnaryArithResHs Neg Natural ': s)

UnaryArithOpHs Neg Bls12381Fr

Defined in Lorentz.Arith

Associated Types

type UnaryArithResHs Neg Bls12381Fr

Methods

evalUnaryArithOpHs :: forall (s :: [Type]). (Bls12381Fr ': s) :-> (UnaryArithResHs Neg Bls12381Fr ': s)

UnaryArithOpHs Neg Bls12381G1

Defined in Lorentz.Arith

Associated Types

type UnaryArithResHs Neg Bls12381G1

Methods

evalUnaryArithOpHs :: forall (s :: [Type]). (Bls12381G1 ': s) :-> (UnaryArithResHs Neg Bls12381G1 ': s)

UnaryArithOpHs Neg Bls12381G2

Defined in Lorentz.Arith

Associated Types

type UnaryArithResHs Neg Bls12381G2

Methods

evalUnaryArithOpHs :: forall (s :: [Type]). (Bls12381G2 ': s) :-> (UnaryArithResHs Neg Bls12381G2 ': s)

UnaryArithOpHs Neq Integer

Defined in Lorentz.Arith

Associated Types

type UnaryArithResHs Neq Integer

Methods

evalUnaryArithOpHs :: forall (s :: [Type]). (Integer ': s) :-> (UnaryArithResHs Neq Integer ': s)

UnaryArithOpHs Neq Natural

Defined in Lorentz.Arith

Associated Types

type UnaryArithResHs Neq Natural

Methods

evalUnaryArithOpHs :: forall (s :: [Type]). (Natural ': s) :-> (UnaryArithResHs Neq Natural ': s)

UnaryArithOpHs Not Bool

Defined in Lorentz.Arith

Associated Types

type UnaryArithResHs Not Bool

Methods

evalUnaryArithOpHs :: forall (s :: [Type]). (Bool ': s) :-> (UnaryArithResHs Not Bool ': s)

UnaryArithOpHs Not Integer

Defined in Lorentz.Arith

Associated Types

type UnaryArithResHs Not Integer

Methods

evalUnaryArithOpHs :: forall (s :: [Type]). (Integer ': s) :-> (UnaryArithResHs Not Integer ': s)

UnaryArithOpHs Not Natural

Defined in Lorentz.Arith

Associated Types

type UnaryArithResHs Not Natural

Methods

evalUnaryArithOpHs :: forall (s :: [Type]). (Natural ': s) :-> (UnaryArithResHs Not Natural ': s)

UnaryArithOpHs Neg (Fixed p)

Defined in Lorentz.Arith

Associated Types

type UnaryArithResHs Neg (Fixed p)

Methods

evalUnaryArithOpHs :: forall (s :: [Type]). (Fixed p ': s) :-> (UnaryArithResHs Neg (Fixed p) ': s)

UnaryArithOpHs Neg (NFixed p)

Defined in Lorentz.Arith

Associated Types

type UnaryArithResHs Neg (NFixed p)

Methods

evalUnaryArithOpHs :: forall (s :: [Type]). (NFixed p ': s) :-> (UnaryArithResHs Neg (NFixed p) ': s)

class DefUnaryArithOp aop where

Helper typeclass that provides default definition of evalUnaryArithOpHs.

Methods

defUnaryArithOpHs :: (UnaryArithOp aop n, r ~ UnaryArithRes aop n) => Instr (n ': s) (r ': s)

Instances

DefUnaryArithOp Abs

Defined in Lorentz.Arith

Methods

defUnaryArithOpHs :: forall (n :: T) (r :: T) (s :: [T]). (UnaryArithOp Abs n, r ~ UnaryArithRes Abs n) => Instr (n ': s) (r ': s)

DefUnaryArithOp Eq'

Defined in Lorentz.Arith

Methods

defUnaryArithOpHs :: forall (n :: T) (r :: T) (s :: [T]). (UnaryArithOp Eq' n, r ~ UnaryArithRes Eq' n) => Instr (n ': s) (r ': s)

DefUnaryArithOp Ge

Defined in Lorentz.Arith

Methods

defUnaryArithOpHs :: forall (n :: T) (r :: T) (s :: [T]). (UnaryArithOp Ge n, r ~ UnaryArithRes Ge n) => Instr (n ': s) (r ': s)

DefUnaryArithOp Gt

Defined in Lorentz.Arith

Methods

defUnaryArithOpHs :: forall (n :: T) (r :: T) (s :: [T]). (UnaryArithOp Gt n, r ~ UnaryArithRes Gt n) => Instr (n ': s) (r ': s)

DefUnaryArithOp Le

Defined in Lorentz.Arith

Methods

defUnaryArithOpHs :: forall (n :: T) (r :: T) (s :: [T]). (UnaryArithOp Le n, r ~ UnaryArithRes Le n) => Instr (n ': s) (r ': s)

DefUnaryArithOp Lt

Defined in Lorentz.Arith

Methods

defUnaryArithOpHs :: forall (n :: T) (r :: T) (s :: [T]). (UnaryArithOp Lt n, r ~ UnaryArithRes Lt n) => Instr (n ': s) (r ': s)

DefUnaryArithOp Neg

Defined in Lorentz.Arith

Methods

defUnaryArithOpHs :: forall (n :: T) (r :: T) (s :: [T]). (UnaryArithOp Neg n, r ~ UnaryArithRes Neg n) => Instr (n ': s) (r ': s)

DefUnaryArithOp Neq

Defined in Lorentz.Arith

Methods

defUnaryArithOpHs :: forall (n :: T) (r :: T) (s :: [T]). (UnaryArithOp Neq n, r ~ UnaryArithRes Neq n) => Instr (n ': s) (r ': s)

DefUnaryArithOp Not

Defined in Lorentz.Arith

Methods

defUnaryArithOpHs :: forall (n :: T) (r :: T) (s :: [T]). (UnaryArithOp Not n, r ~ UnaryArithRes Not n) => Instr (n ': s) (r ': s)

class ToIntegerArithOpHs (n :: Type) where

Minimal complete definition

Nothing

Methods

evalToIntOpHs :: (n ': s) :-> (Integer ': s)

default evalToIntOpHs :: ToIntArithOp (ToT n) => (n ': s) :-> (Integer ': s)

Instances

ToIntegerArithOpHs Natural

Defined in Lorentz.Arith

Methods

evalToIntOpHs :: forall (s :: [Type]). (Natural ': s) :-> (Integer ': s)

ToIntegerArithOpHs Bls12381Fr

Defined in Lorentz.Arith

Methods

evalToIntOpHs :: forall (s :: [Type]). (Bls12381Fr ': s) :-> (Integer ': s)

ToIntegerArithOpHs (NFixed a)

Defined in Lorentz.Arith

Methods

evalToIntOpHs :: forall (s :: [Type]). (NFixed a ': s) :-> (Integer ': s)