Lean 4 Crash Course

def age : Nat := 25
def name : String := "Tomo"
def active : Bool := true
def ratio : Float := 3.14
def ch : Char := 'A'

def age := 25          -- Lean infers Nat
def name := "Tomo"     -- Lean infers String

-- Arithmetic
#eval 10 + 3       -- 13
#eval 10 - 3       -- 7    (Nat subtraction floors at 0: 3 - 10 = 0)
#eval 10 * 3       -- 30
#eval 10 / 3       -- 3    (integer division)
#eval 10 % 3       -- 1    (modulo)

-- Comparison (returns Bool)
#eval 3 < 5        -- true
#eval 3 > 5        -- false
#eval 3 <= 3       -- true
#eval 3 >= 5       -- false
#eval 3 == 5       -- false
#eval 3 != 5       -- true

-- Conversion
#eval (5 : Int)           -- Int from Nat
#eval Int.toNat (-3)      -- 0 (clamps)
#eval Int.toNat 5         -- 5
#eval Nat.toFloat 42      -- 42.0

-- Nat-specific
#eval Nat.min 3 5    -- 3
#eval Nat.max 3 5    -- 5
#eval Nat.pow 2 10   -- 1024
#eval Nat.log2 1024  -- 10
#eval Nat.gcd 12 8   -- 4

#eval true && false    -- false (and)
#eval true || false    -- true  (or)
#eval !true            -- false (not)
#eval true == false    -- false

def s := "hello"

-- Info
#eval s.length          -- 5
#eval s.isEmpty         -- false
#eval "".isEmpty        -- true

-- Combine
#eval s ++ " world"     -- "hello world"
#eval s.append " world" -- "hello world"
#eval String.join ["a", "b", "c"]  -- "abc"
#eval ",".intercalate ["a", "b"]   -- "a,b"

-- Search
#eval s.startsWith "he" -- true
#eval s.endsWith "lo"   -- true
#eval s.contains 'l'    -- true

-- Transform
#eval s.toUpper         -- "HELLO"
#eval s.toLower         -- "hello"
#eval s.trim            -- removes whitespace
#eval s.replace "l" "r" -- "herro"
#eval s.drop 2          -- "llo"
#eval s.take 3          -- "hel"

-- Convert
#eval s.toList          -- ['h', 'e', 'l', 'l', 'o']
#eval s.toUTF8          -- ByteArray
#eval toString 42       -- "42"

-- Split
#eval "a,b,c".splitOn ","     -- ["a", "b", "c"]

-- String interpolation
#eval s!"1 + 1 = {1 + 1}"    -- "1 + 1 = 2"

#eval 'A'.toNat     -- 65
#eval 'a'.isAlpha   -- true
#eval '3'.isDigit   -- true
#eval 'A'.isUpper   -- true
#eval 'a'.isLower   -- true
#eval 'A'.toLower   -- 'a'
#eval Char.ofNat 65 -- 'A'

def bs := ByteArray.mk #[0x48, 0x65]

#eval bs.size              -- 2
#eval bs.get! 0            -- 72 (0x48)
#eval bs.push 0x6C         -- appends byte
#eval bs.extract 0 1       -- sub-array [start, end)
#eval bs.append bs         -- concatenate
#eval bs ++ bs             -- same as append
#eval ByteArray.empty      -- empty
#eval bs.toList            -- [72, 101]

def add (x : Nat) (y : Nat) : Nat :=
  x + y

#eval add 3 5    -- 8

-- These are identical:
def add (x : Nat) (y : Nat) : Nat := x + y
def add (x y : Nat) : Nat := x + y

def compute (x : Nat) : Nat :=
  let doubled := x * 2
  let offset := doubled + 10
  offset                        -- this is returned

def distance (x1 y1 x2 y2 : Nat) : Nat :=
  diff x1 x2 + diff y1 y2
where
  def diff (a b : Nat) : Nat := if a > b then a - b else b - a

-- Full
fun x => x + 1

-- With type
fun (x : Nat) => x + 1

-- Multiple args
fun x y => x + y

-- The · shorthand (type \. in VS Code)
(· + 1)              -- same as fun x => x + 1
(· + ·)              -- same as fun x y => x + y
(· > 3)              -- same as fun x => x > 3

-- These are the same:
[1,2,3].map (· + 10)
[1,2,3].map (fun x => x + 10)

-- Nat → Nat means "takes a Nat, returns a Nat"
-- Nat → Nat → Nat means "takes two Nats, returns a Nat"
#check add    -- Nat → Nat → Nat

-- Each constructor IS a function:
inductive Shape where
  | circle : Nat → Shape             -- circle is a function: Nat → Shape
  | rectangle : Nat → Nat → Shape   -- Nat → Nat → Shape
  | point : Shape                    -- a value (no args)

def max (a b : Nat) : Nat :=
  if a > b then a else b

-- Multi line
def classify (n : Nat) : String :=
  if n == 0 then
    "zero"
  else if n < 10 then
    "small"
  else
    "big"

if h : b = 0 then
  -- h is a proof that b = 0
  0
else
  -- h is a proof that b ≠ 0
  a / b

-- Function REQUIRES proof that divisor isn't zero
def safeDivide (a b : Nat) (proof : b ≠ 0) : Nat := a / b

if h : b = 0 then 0
else safeDivide a b h     -- h proves b ≠ 0

structure Point where
  x : Nat
  y : Nat

def p1 : Point := { x := 3, y := 5 }       -- named fields
def p2 := Point.mk 3 5                       -- .mk constructor (positional)
def p3 : Point := ⟨3, 5⟩                     -- anonymous constructor

#eval p1.x      -- 3
#eval p1.y      -- 5

-- Functional update (creates new value, original unchanged)
def moved := { p1 with x := 10 }
#eval moved.x   -- 10
#eval moved.y   -- 5 (unchanged)

structure Config where
  port : Nat := 8080
  host : String := "localhost"
  debug : Bool := false

def c : Config := { port := 3000 }    -- host and debug use defaults

structure Entry where
  name : String
  value : Nat
  deriving DecidableEq, Repr, Inhabited, BEq, Hashable

structure Commit where
  «from» : PubKey        -- from is reserved in Lean
  type : String
  seq : Nat

-- Access:
commit.«from»

inductive Direction where
  | north | south | east | west

inductive Shape where
  | circle    : Nat → Shape              -- carries a radius
  | rectangle : Nat → Nat → Shape        -- carries width and height
  | point     : Shape                    -- carries nothing

-- Constructing = calling the function:
def s1 := Shape.circle 10
def s2 := Shape.rectangle 3 5
def s3 := Shape.point

-- Function syntax: | patterns directly
def describe : Shape → String
  | .circle r      => "circle with radius " ++ toString r
  | .rectangle w h => toString w ++ "x" ++ toString h
  | .point         => "point"

-- Match syntax: explicit match expression
def describe (s : Shape) : String :=
  match s with
  | .circle r      => "circle with radius " ++ toString r
  | .rectangle w h => toString w ++ "x" ++ toString h
  | .point         => "point"

def canDo : String → Op → Bool
  | "Owner", .C => true
  | "Owner", .R => true
  | "Any",   .R => true
  | _,       _  => false      -- _ means "anything else"

inductive Tree where
  | leaf : Nat → Tree                 -- end point, holds a number
  | node : Tree → Tree → Tree         -- branches into two sub-trees

-- Recursive function walks the tree:
def Tree.sum : Tree → Nat
  | .leaf n   => n                    -- base case: return the number
  | .node l r => l.sum + r.sum        -- recursive: sum both children

def x : Option Nat := some 42
def y : Option Nat := none

-- Extract
#eval x.get!             -- 42 (panics on none — dangerous)
#eval x.getD 0           -- 42 (returns default on none — safe)
#eval y.getD 0           -- 0

-- Check
#eval x.isSome           -- true
#eval x.isNone           -- false

-- Transform without unwrapping
#eval x.map (fun n => n + 1)     -- some 43
#eval y.map (fun n => n + 1)     -- none (function never runs)

-- Filter
#eval x.filter (fun n => n > 10) -- some 42
#eval x.filter (fun n => n > 50) -- none

-- Convert
#eval x.toList           -- [42]
#eval y.toList           -- []

def addFirstTwo (xs : List Nat) : Option Nat := do
  let a ← xs.get? 0      -- ← unwraps Option. If none, whole do returns none
  let b ← xs.get? 1
  return a + b

#eval addFirstTwo [10, 20, 30]    -- some 30
#eval addFirstTwo [10]             -- none (no second element)
#eval addFirstTwo []               -- none

def xs : List Nat := [1, 2, 3, 4, 5]
def empty : List Nat := []
def range := List.range 5              -- [0, 1, 2, 3, 4]
def repeated := List.replicate 3 "x"   -- ["x", "x", "x"]

#eval xs.map (fun x => x * 2)           -- [2, 4, 6, 8, 10]
#eval xs.filter (fun x => x > 3)        -- [4, 5]
#eval xs.reverse                         -- [5, 4, 3, 2, 1]
#eval xs.take 3                          -- [1, 2, 3]
#eval xs.drop 3                          -- [4, 5]
#eval xs.zip [10, 20, 30]               -- [(1,10), (2,20), (3,30)]
#eval xs.enum                            -- [(0,1), (1,2), (2,3), ...]

#eval xs.foldl (fun acc x => acc + x) 0  -- 15 (sum)
#eval xs.any (fun x => x > 4)     -- true
#eval xs.all (fun x => x > 0)     -- true
#eval xs.contains 3                -- true
#eval xs.find? (fun x => x > 3)   -- some 4

#eval [1, 2] ++ [3, 4]            -- [1, 2, 3, 4] (append)
#eval 0 :: [1, 2, 3]              -- [0, 1, 2, 3] (cons: prepend one)
#eval [[1,2], [3,4]].join         -- [1, 2, 3, 4] (flatten)
#eval [3, 1, 4, 1, 5].mergeSort   -- [1, 1, 3, 4, 5]

-- Cons in pattern matching splits a list:
def sum : List Nat → Nat
  | []      => 0                -- empty list
  | x :: xs => x + sum xs       -- x is first, xs is the rest

def arr : Array Nat := #[1, 2, 3, 4, 5]

#eval arr.size         -- 5 (Array uses .size, List uses .length)
#eval arr.get! 2       -- 3
#eval arr.push 6       -- #[1, 2, 3, 4, 5, 6]
#eval arr.pop          -- #[1, 2, 3, 4]
#eval arr.set! 0 99    -- #[99, 2, 3, 4, 5]
#eval arr.map (fun x => x * 2)   -- #[2, 4, 6, 8, 10]
#eval arr.filter (fun x => x > 3)  -- #[4, 5]
#eval arr.reverse      -- #[5, 4, 3, 2, 1]

def pair : Nat × String := (42, "hello")

#eval pair.1    -- 42
#eval pair.2    -- "hello"

-- Destructure
let (a, b) := pair
#eval a    -- 42

-- Triple
def triple : Nat × String × Bool := (1, "hi", true)
#eval triple.1       -- 1
#eval triple.2.1     -- "hi"
#eval triple.2.2     -- true

open Std

def m := HashMap.empty.insert "a" 1 |>.insert "b" 2

#eval m.find? "a"       -- some 1
#eval m.find? "z"       -- none
#eval m.contains "a"    -- true
#eval m.size            -- 2
#eval m.erase "a"       -- removes key
#eval m.toList          -- [("a", 1), ("b", 2)]

-- Take 5, then toString, then get length
#eval 5 |> toString |> String.length    -- 1

-- Sort, then reverse, then get first
#eval [3, 1, 2] |>.mergeSort |>.reverse |>.head!   -- 3

structure ByteVec (n : Nat) where
  data : ByteArray
  size_eq : data.size = n

abbrev Hash := ByteVec 32       -- exactly 32 bytes
abbrev PubKey := ByteVec 32     -- exactly 32 bytes
abbrev Signature := ByteVec 64  -- exactly 64 bytes

-- Non-empty list
structure NonEmptyList (a : Type) where
  data : List a
  nonempty : data.length > 0

-- Bounded number
structure Port where
  value : Nat
  low : value >= 1
  high : value <= 65535

-- Valid email
structure Email where
  value : String
  hasAt : value.contains '@' = true

inductive Vec (a : Type) : Nat → Type where
  | nil  : Vec a 0                        -- empty = length 0
  | cons : a → Vec a n → Vec a (n + 1)    -- prepend = length + 1

-- Only works on non-empty Vec (n + 1, not 0)
def head : Vec a (n + 1) → a
  | .cons x _ => x

-- Zipping requires SAME length (both n)
def zip : Vec a n → Vec b n → Vec (a × b) n
  | .nil, .nil => .nil
  | .cons a as, .cons b bs => .cons (a, b) (zip as bs)

-- namespace — adds a prefix
namespace Utils
  def helper := 42
end Utils
#eval Utils.helper     -- need prefix

-- open — removes the prefix
open Utils
#eval helper           -- no prefix

-- section — groups without prefix
section MyProofs
  variable (n : Nat)       -- n available to all in section

  theorem ex1 : n + 0 = n := by simp
  theorem ex2 : n * 1 = n := by simp
end MyProofs
-- n is gone here

-- Transparent alias (compiler sees through it)
abbrev Hash := ByteVec 32
-- Hash and ByteVec 32 are interchangeable everywhere

-- Opaque alias (distinct type)
def Score := Nat
-- Score and Nat are NOT interchangeable

class Printable (a : Type) where
  print : a → String

instance : Printable Nat where
  print n := toString n

instance : Printable Bool where
  print b := if b then "yes" else "no"

-- [Printable a] means "a must have a Printable instance"
def show [Printable a] (x : a) : String := Printable.print x

#eval show 42        -- "42"
#eval show true      -- "yes"

class AppManifest (A : Type) where
  name          : String
  schema        : Schema
  eventTypes    : List String
  -- Proof obligations — must be satisfied by every instance
  all_creatable : ∀ et, et ∈ eventTypes → ∃ role, schema.permits role et .C = true
  roles_valid   : ∀ r, r ∈ customRoles → r ≠ "Self" ∧ r ≠ "Owner"

class AppMiddleware (K : Type) where
  encrypt   : K → ByteArray → ByteArray
  decrypt   : K → ByteArray → Option ByteArray
  -- Roundtrip proof: decrypt(encrypt(m)) = m
  roundtrip : ∀ k m, decrypt k (encrypt k m) = some m

instance : AppManifest TimelineConfig where
  name := "timeline"
  schema := timelineSchema
  eventTypes := ["Timeline_Post", "Timeline_Profile", ...]
  all_creatable := by
    intro et het
    simp [List.Mem] at het
    rcases het with rfl | rfl | rfl
    · exact ⟨"Owner", by native_decide⟩
    · exact ⟨"Owner", by native_decide⟩
    · exact ⟨"Any", by native_decide⟩
  roles_valid := by
    intro r hr; simp [List.Mem] at hr
    rcases hr with rfl | rfl
    · constructor <;> decide
    · constructor <;> decide

class DirectMiddleware (K : Type) extends AppMiddleware K where
  agree     : ByteVec 32 → PubKey → K
  agree_sym : ∀ a b, agree a b = agree b a

-- ENCApp bundles everything — if it exists, the app is valid
class ENCApp (A W K Idx Q S : Type) extends
    AppManifest A, AppSDK A W, AppMiddleware K,
    AppDataView A Idx Q, AppState S, AppComponents A W

-- sha256 is an axiom — no implementation exists in Lean
axiom sha256 : ByteArray → Hash

-- Anything using sha256 must be noncomputable
noncomputable def H (fields : List CborField) : Hash :=
  sha256 (cborEncode fields)

-- Instances using axiomatized functions also need noncomputable
noncomputable instance : AppSDK TimelineConfig TimelineWrite where
  buildCommit := fun w id enc exp => ...    -- uses axiom-based SDK functions

FTA (abstract)     class FTA.CryptoSuite, class FTA.App
  ↓ instance
ENC (protocol)     class AppManifest, AppSDK, AppMiddleware, ...
  ↓ instance
Apps               instance : AppManifest TimelineConfig, ...

def main : IO Unit := do
  IO.println "What is your name?"
  let name ← IO.getStdin >>= (·.getLine)
  IO.println s!"Hello, {name}"

#eval s!"1 + 1 = {1 + 1}"    -- "1 + 1 = 2"
#eval s!"name: {"Tomo"}"      -- "name: Tomo"

import Enc.Core.Primitives       -- load module
open Enc.RBAC                     -- bring names into scope

Enc/Core/Primitives.lean   →  import Enc.Core.Primitives
Enc/Apps/Timeline/App.lean →  import Enc.Apps.Timeline.App

-- Barrel re-export:
-- Enc/Core/Primitives.lean
import Enc.Core.Primitives.Types
import Enc.Core.Primitives.Crypto
import Enc.Core.Primitives.Hash
-- importing Primitives imports all three

#check Nat                -- Nat : Type           (what is this?)
#check (3 : Nat)          -- 3 : Nat
#check Nat.add            -- Nat → Nat → Nat     (function signature)
#check @List.map          -- full type with all implicit args

#eval 2 + 3              -- 5                     (run and print)
#eval [1,2,3].map (fun x => x * 2)   -- [2, 4, 6]

#print Nat.add            -- shows the definition
#print axioms H_injective -- shows which axioms a theorem depends on