adolfont · October 22, 2023 21:24 · adolfont · Oct 22, 2023
diff --git a/fpinlean.lean b/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 :=
	α