/- Exercise 1.1: Basics — Definitions and Propositions -/
/- Replace the placeholders (e.g. `:= sorry`) with your solutions. -/
/- Question 1: Fibonacci numbers -/
/- 1.1. Define the function `fib` that returns the Fibonacci numbers. -/
def fib : ℕ → ℕ
:= sorry
/- 1.2. Check that your function works as expected. -/
#reduce fib 0 -- expected: 0
#reduce fib 1 -- expected: 1
#reduce fib 2 -- expected: 1
#reduce fib 3 -- expected: 2
#reduce fib 4 -- expected: 3
#reduce fib 5 -- expected: 5
#reduce fib 6 -- expected: 8
/- Question 2: Arithmetic Expressions -/
/- 2.1. Define an inductive type `aexp` to represent arithmetic expressions.
It should be equipped with six constructors:
* `num` takes an integer (ℤ = \int) and represents that integer;
* `var` takes a string and represents a variable of that name;
* `add`, `sub`, `mul`, `div` take two arithmetic expressions and represent
the operations +, -, *, and /, respectively.
-/
-- enter your solution here
/- 2.2. Define an evaluation function `eval` that takes an environment, giving
the value of variables, and an arithmetic expression and that returns an
integer. -/
def eval (env : string → ℤ) : aexp → ℤ
:= sorry
/- 2.3. Test `eval` on some examples, making sure to exercise each constructor
at least once. You can use the following environment in your tests. -/
def some_env : string → ℤ
| "x" := 3
| "y" := 17
| _ := 201
-- invoke `#reduce` here