Az Idris programozási nyelv

Nyelvi elemek

Jelkészlet

Az Idrisben ugyanaz a jelkészlet használható, amely Haskellben, azaz Unicode 3.0. A kis- és nagybetűket a fordító megkülönbözteti. A nyelv úgynevezett margó szabályos nyelv (szintén a Haskellhez hasonlóan), azaz az egyes blokkokat az indentálás jelzi.

Azonosítók

Változók, függvénynevek: kisbetűvel kezdődik, utána 0 vagy több betű, aláhúzás, számjegy vagy aposztróf állhat.

Típusnév, konstruktor: nagybetűvel kezdődik, utána 0 vagy több betű, aláhúzás, számjegy vagy aposztróf állhat.

Literálok

Megjegyzések

A -- jelek segítségével egysoros megjegyzést, a {- és -} jelek között több soron keresztül tartó megjegyzést írhatunk, az utóbbi változat egymásba is ágyazható. Dokumentációs megjegyzések jelenleg még nincsenek, viszont az Idris közösség körében már folynak az igényfelmérések, hogy ki milyen típusú dokumentációs megjegyzés sémát részesítene előnyben.

Literális programozás

Az Idris támogatja a literális programozást is, mely azt jelenti, hogy csak a ">" jellel kezdődő sorok programsorok, minden más komment. Ha ezt a módot akarjuk használni, akkor a .lidr kiterjesztést kell adnunk programfájljainknak.