This commit is contained in:
2025-11-19 11:15:50 +01:00
parent d91a947186
commit 773fe1a9c3

View File

@ -98,13 +98,10 @@ Hint: If you want to make use of addition in the implementation of multiplicatio
{ Zero() -> Zero()
; Succ(n) -> add m (mult n)
}
#+end_src
where we substitute ~add~ for the following:
#+begin_src chi
\m. rec add = \n. case n of
{ Zero() -> m
; Succ(n) -> Suc(add n)
}
[ add <- \m. rec add = \n. case n of
{ Zero() -> m
; Succ(n) -> Suc(add n)
}]
#+end_src
** (2p) [BN]