Basics.md (1217B)
1 +++ 2 title = 'Basics' 3 template = 'page-math.html' 4 +++ 5 # Basics 6 ## Type checking 7 8 Type checking is done using rules: 9 10 Constant: 11 12 $\overline{C \vdash c : \sigma}^{\enspace Cst}$ if c declared with type $\sigma$ 13 14 Variable: 15 16 $\overline{C \vdash x : \sigma}^{\enspace Var}$ if $x : \sigma$ occurs in C 17 18 Application: 19 20 $ 21 \underline{C \vdash t : \sigma \rightarrow \tau \qquad C \vdash u : \sigma}_{\enspace App} \\\\ 22 C \vdash t u : \tau 23 $ 24 25 Lambda: 26 27 $ 28 C, x : \sigma \vdash t : \tau \\\\ 29 \overline{C \vdash (\lambda x : \sigma, t) : \sigma \rightarrow \tau}^{\enspace Lam} 30 $ 31 32 ## Lean diagnosis commands 33 * `#check`: checks the type of something 34 * `#print`: prints the definition of something 35 * `#eval`: evaluates something 36 37 You can use the placeholder `_`, Lean will help you by telling you what needs to be found. 38 39 ## Inductive type definitions 40 For example, arithmethic expressions: 41 42 ```lean 43 inductive aexp : Type 44 | num : ℤ → aexp 45 | var : string → aexp 46 | add : aexp → aexp → aexp 47 | sub : aexp → aexp → aexp 48 | mul : aexp → aexp → aexp 49 | div : aexp → aexp → aexp 50 ``` 51 52 ## Function definitions 53 For example a power function: 54 55 ```lean 56 def power : ℕ → ℕ → ℕ 57 | _ 0 := 1 58 | m (n+1) := m * (power m n) 59 ```