Nobody has mentioned the dependently type prog-lang Epigram† yet? “Epigram uses a two-dimensional, natural deduction style syntax, with a LaTeX version and an

Nobody has mentioned the dependently type prog-lang Epigram† yet? “Epigram uses a two-dimensional, natural deduction style syntax, with a LaTeX version and an ASCII version. Here are some examples from The Epigram Tutorial: Examples The natural numbers The following declaration defines the natural numbers:” ( ! ( ! ( n : Nat ! data !---------! where !----------! ; !-----------! ! Nat : * ) !zero : Nat) !suc n : Nat) “The declaration says that Nat is a type with kind * (i.e., it is a simple type) and two constructors: zero and suc. The constructor suc takes a single Nat argument and returns a Nat. This is equivalent to the Haskell declaration "data Nat = Zero | Suc Nat".” Project lives here: https://code.google.com/archive/p/epigram/ https://code.google.com/archive/p/epigram/ and the last commit on https://github.com/mietek/epigram2 https://github.com/mietek/epigram2 is five years ago which leads me to believe that the project is abandon-ware. † https://en.wikipedia.org/wiki/Epigram_(programming_language) https://en.wikipedia.org/wiki/Epigram_(programming_language)