1  -- 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".
  2  def joinStringsWith (a : String) (b : String) (c : String) :String :=
  3    String.append b (String.append a c)
  4  
  5  #check (joinStringsWith)
  6  #eval joinStringsWith ", " "one" "and another"
  7  
  8  -- What is the type of joinStringsWith ": " ? Check your answer with Lean.
  9  #check joinStringsWith ": "
 10  
 11  -- Define a function `volume` with type Nat->Nat->Nat->Nat that computes the volume of a rectangular prism with the given hight, width and depth.
 12  def volume (width : Nat) (height : Nat) (depth : Nat) : Nat :=
 13    width * height * depth
 14  
 15  #check (volume)
 16  
 17  
 18  #check 1
 19  #eval 1
 20  
 21  def myStr : Type := String
 22  #check myStr
 23  #eval myStr
 24  
 25  -- 1.4 Structures
 26  
 27  structure Point where
 28    x : Float
 29    y : Float
 30  
 31  structure PointPolar where
 32    x : Float
 33    y : Float
 34  
 35  
 36  
 37  #check Point
 38  
 39  #eval ({x:=1, y:=2} : Point)
 40  
 41  #check PointPolar
 42  
 43  def origin : Point := {x:=0, y:=0}
 44  #eval origin
 45  
 46  -- 1.4.3. Exercise
 47  
 48  -- Define a structure named RectangularPrism that contains the height,
 49  -- width, and depth of a rectangular prism, each as a Float.
 50  
 51  structure RectangularPrism where
 52    height: Float
 53    width: Float
 54    depth: Float
 55  
 56  -- Define a function named volume : RectangularPrism → Float
 57  -- that computes the volume of a rectangular prism.
 58  
 59  def volumeRP (rp : RectangularPrism) : Float :=
 60    rp.height * rp.width * rp.depth
 61  
 62  #check (volumeRP)
 63  
 64  -- Define a structure named Segment that represents a line segment by its endpoints,
 65  -- and define a function length : Segment → Float that computes the
 66  -- length of a line segment. Segment should have at most two fields.
 67  
 68  structure Segment where
 69    p1: Point
 70    p2: Point
 71  
 72  def length (seg : Segment) : Float :=
 73    Float.sqrt (((seg.p1.x - seg.p2.x)^2) + ((seg.p1.y - seg.p2.y)^2))
 74  
 75  def zero : Point := {x:=0, y:=0}
 76  def unitx : Point := {x:=1, y:=0}
 77  def unity : Point := {x:=0, y:=1}
 78  
 79  def x_unit_seg : Segment := {p1 := zero, p2:= unitx}
 80  
 81  #eval length x_unit_seg
 82  #eval length {p1:= unity, p2:= zero}
 83  #eval length {p1:= unitx, p2:=unity}
 84  #eval length {p1:= unity, p2:=unitx}
 85  
 86  -- Which names are introduced by the declaration of RectangularPrism?
 87  
 88  #check (RectangularPrism.mk)
 89  #check (RectangularPrism.depth)
 90  #check (RectangularPrism.height)
 91  #check (RectangularPrism.width)
 92  
 93  -- Which names are introduced by the following declarations of `Hamster` and `Book`?
 94  -- What are their types?
 95  
 96  structure Hamster where
 97    name : String
 98    fluffy : Bool
 99  
100  -- Hamster.mk : String -> Bool -> Hamster
101  -- Hamster.name : Hamster -> String
102  -- Hamster.fluffy : Hamster -> Bool
103  
104  #check (Hamster.fluffy)
105  #eval Hamster.fluffy {name:="name1", fluffy:=true}
106  
107  structure Book where
108    makeBook ::
109    title : String
110    author :String
111    price:Float
112  
113  #check (Book.makeBook) -- String->String->Float->Book
114  #check (Book.title) -- Book -> String
115  
116  
117  -- 1.5.1 Pattern Matching
118  def bookPriceAccessor (book: Book) : Float :=
119    book.price
120  
121  def bookPriceMatch( book:Book) : Float :=
122    match book with
123      | {title:=a, author:=b, price:=p} => p
124  
125  def bookPriceProjector (book: Book) : Float :=
126    Book.price book
127  
128  
129  
130  #eval bookPriceAccessor {title:= "a", author:="b", price:=100.0}
131  #eval bookPriceMatch {title:= "a", author:="b", price:=100.0}
132  #eval bookPriceProjector {title:= "a", author:="b", price:=100.0}