| 12345678910111213141516171819202122232425262728293031323334 |
- EXECUTED_PROGRAM
- ret > ExitSuccess
- out > Word.NumWord =
- out > Agda.Builtin.FromNat.Number.constructor _ (λ a _ → toWord64 a)
- out > Word.NumNat = Agda.Builtin.FromNat.Number.constructor _ (λ a _ → a)
- out > Word.natOp = λ a b c → toWord64 (a (fromWord64 b) (fromWord64 c))
- out > Word._^_ =
- out > λ a b →
- out > case b of
- out > 0 → 1
- out > _ → let c = b - 1 in a * Word._^_ a c
- out > Word.2⁶⁴ = Word._^_ 2 64
- out > Word.addWord = λ a b → a +64 b
- out > Word.subWord = λ a b → a -64 b
- out > Word.mulWord = λ a b → a *64 b
- out > Word.NonZero = _
- out > Word.div = λ a b _ → quot a b
- out > Word.mod = λ a b _ → rem a b
- out > Word.NonZeroWord = _
- out > Word.divWord = λ a b _ → quot64 a b
- out > Word.modWord = λ a b _ → rem64 a b
- out > Word.eqWord = λ a b → a ==64 b
- out > Word.ltWord = λ a b → a <64 b
- out > Word.2^63 = 1 +64 quot64 (0 -64 1) 2
- out > Word.test = 100 +64 Word.2^63 +64 (1 +64 Word.2^63)
- out > Word.prf = _
- out > Word.prf' = _
- out > Word.main = Word.putStrLn (Word.showWord Word.test)
- out > Word.ltDouble = λ a b → 2 *64 a <64 b
- out > Word.lt4x = λ a _ → let b = 2 *64 a in seq b (Word.ltDouble b) b
- out > 101
- out >
|
