Lean

A functional programming language that makes it easy to write correct and maintainable code.

Website | Source | Docs | Theorem Proving in Lean | Functional Programming in Lean

Lean has numerous features, including:

Example:

-- Defines a function that takes a name and produces a greeting.
def getGreeting (name : String) := s!"Hello, {name}! Isn't Lean great?"

-- The `main` function is the entry point of your program.
-- Its type is `IO Unit` because it can perform `IO` operations (side effects).
def main : IO Unit :=
  -- Define a list of names
  let names := ["Sebastian", "Leo", "Daniel"]

  -- Map each name to a greeting
  let greetings := names.map getGreeting

  -- Print the list of greetings
  for greeting in greetings do
    IO.println greeting

Tags: language   functional  

Last modified 05 February 2024