Commit 081460d5 authored by Raphaël Cauderlier's avatar Raphaël Cauderlier
Browse files

Move casting function between machine and binary numbers to

dk_binary_nat because it is hard to prove confluent and dk_binary_nat is
not checked for confluence.
parent 56e2d0ee
......@@ -116,3 +116,18 @@ def mod2 : BNat -> UNat -> BNat.
[] mod2 O _ --> O
[n,k] mod2 (S0 n) (dk_nat.S k) --> S0 (mod2 n k)
[n,k] mod2 (S1 n) (dk_nat.S k) --> S1 (mod2 n k).
(; Casting to machine numbers ;)
def mnat_of_bnat : N : UNat -> bn : BNat -> dk_machine_int.MInt N.
[N] mnat_of_bnat N O --> dk_machine_int.zero N
[ ] mnat_of_bnat dk_nat.O _ --> dk_machine_int.O.
[N,bn]
mnat_of_bnat (dk_nat.S N) (dk_binary_natS0 bn)
-->
dk_machine_int.S0 N (mnat_of_bnat N bn)
[N,bn]
mnat_of_bnat (dk_nat.S N) (dk_binary_natS1 bn)
-->
dk_machine_int.S1 N (mnat_of_bnat N bn).
......@@ -201,16 +201,3 @@ def cast_peano : N : UNat -> n : UNat -> MInt N.
[N] cast_peano N dk_nat.O --> zero N
[N,n] cast_peano N (dk_nat.S n) --> succ N (cast_peano N n).
(; Casting binary natural numbers ;)
def cast_bnat : N : UNat -> bn : dk_binary_nat.BNat -> MInt N.
[N] cast_bnat N dk_binary_nat.O --> zero N
[ ] cast_bnat dk_nat.O _ --> O.
[N,bn]
cast_bnat (dk_nat.S N) (dk_binary_nat.S0 bn)
-->
S0 N (cast_bnat N bn)
[N,bn]
cast_bnat (dk_nat.S N) (dk_binary_nat.S1 bn)
-->
S1 N (cast_bnat N bn).
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment