| 12345678910111213141516171819202122232425262728293031323334353637383940414243 |
- module RTP where
- open import RTN public
- {-
- data Bool : Set where
- False : Bool
- True : Bool
- -}
- postulate
- Int : Set
- String : Set
- Float : Set
- Char : Set
- {-# BUILTIN FLOAT Float #-}
- {-# BUILTIN STRING String #-}
- -- postulate primShowBool : Bool -> String
- postulate primShowInt : Int -> String
- postulate primShowChar : Char -> String
- postulate primStringAppend : String -> String -> String
- postulate primStringReverse : String -> String
- -- postulate primStringToList : String -> List Char
- -- postulate primStringFromList
- -- Int stuff
- postulate primIntZero : Int
- postulate primIntOne : Int
- postulate primIntSucc : Int -> Int
- postulate primNatToInt : Nat -> Int
- postulate primIntToNat : Int -> Nat
- postulate primIntAdd : Int -> Int -> Int
- postulate primIntSub : Int -> Int -> Int
- postulate primIntMul : Int -> Int -> Int
- postulate primIntDiv : Int -> Int -> Int
- postulate primIntMod : Int -> Int -> Int
|
