adolfont/fpinlean.lean

## fpinlean.lean
-- Exercises
-- Functional Programming in Lean
-- https://lean-lang.org/functional_programming_in_lean/getting-to-know/functions-and-definitions.html

-- Define the function joinStringsWith with type String -> String -> String -> String that creates a new string by placing its first argument between its second and third arguments. joinStringsWith ", " "one" "and another" should evaluate to "one, and another".
-- What is the type of joinStringsWith ": "? Check your answer with Lean.
-- Define a function volume with type Nat → Nat → Nat → Nat that computes the volume of a rectangular prism with the given height, width, and depth.

def maximum (n : Nat) (k : Nat) : Nat :=
  if n < k then
    k
  else n

def joinStringsWith (s1: String) (s2: String) (s3: String)  : String :=
   String.append s2 (String.append s1 s3)

#eval joinStringsWith ", " "one" "and another"

#check (joinStringsWith ": ")

def volume (height : Nat) (width : Nat) (depth : Nat) : Nat :=
  height * width * depth

def identity (α: Nat): Nat :=
  α
	-- Exercises
	-- Functional Programming in Lean
	-- https://lean-lang.org/functional_programming_in_lean/getting-to-know/functions-and-definitions.html

	-- Define the function joinStringsWith with type String -> String -> String -> String that creates a new string by placing its first argument between its second and third arguments. joinStringsWith ", " "one" "and another" should evaluate to "one, and another".
	-- What is the type of joinStringsWith ": "? Check your answer with Lean.
	-- Define a function volume with type Nat → Nat → Nat → Nat that computes the volume of a rectangular prism with the given height, width, and depth.

	def maximum (n : Nat) (k : Nat) : Nat :=
	if n < k then
	k
	else n

	def joinStringsWith (s1: String) (s2: String) (s3: String) : String :=
	String.append s2 (String.append s1 s3)

	#eval joinStringsWith ", " "one" "and another"

	#check (joinStringsWith ": ")

	def volume (height : Nat) (width : Nat) (depth : Nat) : Nat :=
	height * width * depth

	def identity (α: Nat): Nat :=
	α