Skip to content

GitLab

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

Fix an error in the definition of dk_binary_nat.mult

parent c8138f22
Hide whitespace changes
Inline Side-by-side
Showing with 2 additions and 2 deletions
dk_binary_nat.dk
View file @ 398522c6
......@@ -80,8 +80,8 @@ def mult : BNat -> BNat -> BNat.
[] mult O _ --> O
[] mult _ O --> O
[n,m] mult (S0 n) (S0 m) --> S0 (S0 (mult n m))
[n,m] mult (S0 n) (S1 m) --> S0 (plus m (S0 (mult n m)))
[n,m] mult (S1 n) (S0 m) --> S0 (plus n (S0 (mult n m)))
[n,m] mult (S0 n) (S1 m) --> S0 (plus (S0 (mult n m)) n)
[n,m] mult (S1 n) (S0 m) --> S0 (plus m (S0 (mult n m)))
[n,m] mult (S1 n) (S1 m) --> S1 (plus (S0 (mult m n)) (plus n m)).
(; Min and Max ;)
......
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