Kind: A Modern Proof Language(github.com)

    blocks :: Entity -> Bool -> Bool
    blocks entity floats True = True
    blocks entity floats False = case entity of
      Creature name hp age items pos -> True
      Tile pos effect isWater -> not isWater || floats
      Wall pos -> True
      Fire pos damage kind -> False

    blocks(entity: Entity, floats: Bool, ghost: Bool): Bool
      case ghost {
        true: true
        false: case entity {
          creature: true
          tile: not(tile.is_water) || floats
          wall: true
          fire: false
        }
      }
          

    let x = some(3) <> 5 // x is 3
    let y = none    <> 5 // x is 5

    sum_first_3(list: List<Nat>): Nat
      x = list[0] abort 0 // returns 0 if x is none
      y = list[1] abort 0
      z = list[2] abort 0
      x + y + z

    sum_first_3(list: List<Nat>): Nat
      Maybe {
        get x = list[0]
        get y = list[1]
        bet z = list[2]
        return x + y + z
      } <> 0

    open vec
    vec.x + vec.y + vec.z

    name = my_list[7]

    name = my_map{"foo"}

    name = my_record@foo

    name = my_list[7] <> "anonymous"

    name = my_list[7] <- "Eric"

    age_factorial(birth:_year Nat, names: List<String>): String
      // Concatenates all names in a string
      name = ""
      name = for name in names:
        name | " " | name

      // Computes the age
      age = current_year - birth_year

      // Computes the factorial of the age
      fact = 1
      fact = for n from 0 to age:
        fact * n

      if age <? 18 then
        "You're too young to use this program"
      else
        "Hello, " | name | ", the factorial of your age is " | fact

  key = "foo"
  map = {key: 3}