st0244-2023-1-lab2

Field	Value
Full name	Luis M. Torres V.
OS	Ubuntu 22.04.01 LTS
GHC	9.6.1
cabal	3.10.1.0
QuickCheck	2.14.2
quickcheck-instances	0.3.29.1

Running test suite

• cabal run for verbose output (per test).

• cabal test for short output (passed or failed).

A note on layout and indentation

I'm using the hindent Haskell pretty printer to format all source files.

I'm assuming it knows better than me.

If there is, for example, a three-spaces indent (as is the case below)

prop_f6 n =
  natToNatural (f6 n') ==
  (if n == 0
     then 0
     else n - 1)
  . . .

then I won't nitpick about that.

Useful sources

1. Examples of primitive recursive functions defined using the recursor in a lambda calculus (pg. 21):

   Bertot, Yves (June 2015). A short overview of Type Theory. https://www-sop.inria.fr/members/Yves.Bertot/misc/slides-eng.pdf

2. Introduction to PRFs with definitions:

   Gómez Marín, Raúl and Sicard Ramírez, Andrés [2001] (2002). Informática Teórica: Elementos propedeúticos. Fondo Editorial Universidad EAFIT. http://www1.eafit.edu.co/asr/pubs/informatica-teorica.html

3. More definitions of PRFs:

   Kleene, Stephen Cole [1952] (1971). Introduction to Metamathematics. North-Holland. Sec. 43, pg. 219.

4. Step-by-step "construction" of the recursor structure for PRFs:

   Dean, Walter, Recursive Functions in The Stanford Encyclopedia of Philosophy (Winter 2021 Edition), Edward N. Zalta (ed.), https://plato.stanford.edu/archives/win2021/entries/recursive-functions/

About

The purpose of this programming lab is to implement five primitive recursive functions using the data type Nat and the recursor recNat in Haskell.