This is the personal website of Jan Marthedal Rasmussen.

The latest update to my micropost feed is the following:

  • Functional Programming in Lean, a free book on using Lean as a programming language lean-lang.org/functional_programmi…

    inductive Vect (α : Type u) : Nat → Type u where
  | nil : Vect α 0
  | cons : α → Vect α n → Vect α (n + 1)

def Vect.zip : Vect α n → Vect β n → Vect (α × β) n
  | .nil, .nil => .nil
  | .cons x xs, .cons y ys => .cons (x, y) (zip xs ys)
    Published

My five latest posts are: