agda/examples/outdated-and-incorrect/Alonzo/PreludeInt.agda

module PreludeInt where
open import AlonzoPrelude
import RTP

int : Nat -> Int
int = RTP.primNatToInt

_+_ : Int -> Int -> Int
_+_ = RTP.primIntAdd


_-_ : Int -> Int -> Int
_-_ = RTP.primIntSub

_*_ : Int -> Int -> Int
_*_ = RTP.primIntMul

div : Int -> Int -> Int
div = RTP.primIntDiv

mod : Int -> Int -> Int
mod = RTP.primIntMod