idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-27 13:43:28 +03:00
Code Issues Projects Releases Wiki Activity
ddcbe795c6
Idris2/tests/idris2/literate010/MyFirstIdrisProgram.org
Edwin Brady a972778eab Add test script 
They don't all pass yet, for minor reasons. Coming shortly...
Unfortunately the startup overhead for chez is really noticeable here!
2020-05-19 18:25:18 +01:00

933 B
Raw Blame History

My First Idris2 Program

This is a literate Idris2 Org-Mode file that the Idris2 understands.

We can have visibile code blocks using source blocks in idris.

data Natural = Zero | Succ Natural
data Vect : Natural -> Type -> Type where
  Empty : Vect Zero a
  Cons  : a -> Vect k a -> Vect (Succ k) a

We can have hidden literate lines that Idris will understand.

However, we Idris2' literate support is greedy and does not understand all of the supported literate modes comments and verbatim blocks.

Thus:

#+IDRIS: plus : Natural -> Natural -> Natural

is also an active code line.

We can also abuse org-mode comments to hide code not required for publication.

cannotSeeThis : Natural -> Natural

main : IO ()
main = putStrLn "Hello!"