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

Typo

parent 5fe6b6dd
......@@ -124,10 +124,10 @@ 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)
mnat_of_bnat (dk_nat.S N) (S0 bn)
-->
dk_machine_int.S0 N (mnat_of_bnat N bn)
[N,bn]
mnat_of_bnat (dk_nat.S N) (dk_binary_natS1 bn)
mnat_of_bnat (dk_nat.S N) (S1 bn)
-->
dk_machine_int.S1 N (mnat_of_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