ꠚꠣꠟꠖꠤꠀ ꠎꠤꠘꠤꠡꠣꠁꠘ꠆ꠔ ꠎꠣꠃꠇ꠆ꠇꠣ

ꠁꠖ꠆ꠞꠤꠍ

<bdi>ꠃꠁꠇꠤꠙꠤꠒꠤꠀ</bdi> ꠕꠘꠦ
( ꠀꠁꠒ꠆ꠞꠤꠡ ꠕꠘꠦ ꠚꠤꠞꠤꠀ ꠀꠁꠍꠦ )

w:WP:STUB ꠁ ꠙꠣꠔꠣ ꠁꠈꠣꠘ ꠀꠛꠧ ꠇꠥꠠꠤ ꠞꠂꠍꠦ ⁕ ꠈꠣꠟꠤ ꠝꠣꠔ ꠃꠑꠣꠘꠤꠞ ꠟꠣꠉꠤ ꠀꠞꠝ꠆ꠛ ꠇꠞꠣ ꠅꠁꠍꠦ ⁕ ꠁꠟꠣꠘ ꠀꠞꠅ ꠘꠄꠀ ꠇꠥꠠꠤꠘ꠆ꠔꠞ ꠙꠣꠔꠣꠁꠘ ꠖꠦꠈꠂꠘ ⁕ ꠁ ꠛꠦꠙꠣꠞꠦ ꠀꠙꠘꠣꠁꠘ꠆ꠔꠞ ꠇꠥꠘꠔꠣ ꠙꠥꠞꠣꠘꠤꠞ ꠕꠣꠇ꠆ꠟꠦ ꠟꠇ꠆ꠖꠤ ꠟꠦꠈꠤꠀ ꠙꠣꠔꠣ ꠁꠈꠣꠘ ꠀꠞꠧ ꠛꠟꠣꠁꠔꠣ ꠙꠣꠞꠂꠘ ⁕

ꠁꠖ꠆ꠞꠤꠍ
ꠎꠦ ꠎꠤꠘꠤꠡꠞpurely functional programming language ꠨ programming language ꠨ dependently typed programming language ꠨ proof assistant
ꠜꠤꠔ꠆ꠔꠤ ꠉꠣꠞꠣ ꠅꠁꠍꠦ
ꠍꠚꠐꠅꠄꠀꠞ ꠜꠣꠞꠡꠘꠞ ꠀꠁꠒꠤ..
ꠎꠦꠐꠣꠄ ꠀꠍꠞ ꠇꠞꠦꠢꠣꠍꠇꠦꠟ ꠨ ꠄꠉꠖꠣ ꠨ Rocq ꠨ Clean ꠨ Epigram
programming paradigmfunctional programming ꠨ purely functional programming ꠨ total functional programming
readable file formatIdris source code file ꠨ Literate Idris source code file
writable file formatIdris source code file ꠨ Literate Idris source code file
programmed inꠢꠣꠍꠇꠦꠟ
source code repository URLhttps://github.com/idris-lang/Idris-dev
ꠅꠚꠤꠡꠤꠀꠟ ꠅꠄꠛꠍꠣꠁꠐhttps://www.idris-lang.org
copyright licenseBSD licenses
typing disciplinedependent typing ꠨ static typing ꠨ linear typing ꠨ uniqueness typing
IRC channel URLirc://libera.chat/#idris
file extensionidr ꠨ lidr
Arch Linux packageidris

ꠁꠖ꠆ꠞꠤꠍ ꠅꠁꠟꠅ ꠄꠉꠥ ꠇꠝ꠆ꠙꠥꠐꠣꠞꠞ ꠜꠣꠡꠣ ⁕

ꠀꠞꠅ ꠖꠦꠈꠂꠘ

[ꠃꠔꠡ ꠟꠦꠈꠁꠘ]

{{{text}}}

    ꠕꠥꠇꠣꠘꠤ

    [ꠃꠔꠡ ꠟꠦꠈꠁꠘ]