sum : List Integer -> Integer
sum Nil = 0
sum (Cons x xs) = x + sum xs


-- Plutus Core w/ global statements, data, etc.

(declare sum (fun (con Prelude.List (integer)) (integer)))
(define sum (lambda xs
  (case xs
    (Prelude.Nil () 0)
    (Prelude.Cons (x xs') [plusInteger x [sum xs]])))


-- Plutus Core w/o global statements, w/ Scott encodings (roughly)

(letrec
  ((declare sum (fun (con Prelude.List (integer)) (integer)))
   (define sum (lambda xs
     (listCase xs
       0
       (lambda x xs' [plusInteger x [sum xs]]))))
  <SCOPE>)





factorial : Integer -> Integer
factorial n =
  if n < 1
  then 1
  else n * factorial (n - 1)


(declare factorial (fun (integer) (integer)))
(define factorial (lambda n
  (case [lessThanInteger n 1]
    (Prelude.True () 1)
    (Prelude.False () [multiplyInteger n [factorial [subtractInteger n 1]]])))


(letrec
  ((declare factorial (fun (integer) (integer)))
   (define factorial (lambda n
     (boolCase [lessThanInteger n 1]
       (lambda u 1)
       (lambda u [multiplyInteger n [factorial [subtractInteger n 1]]]))))
  <SCOPE>)