Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | |||
|
idris_syntax [2017/06/06 13:07] nikolaj |
idris_syntax [2017/06/06 13:08] nikolaj old revision restored (2016/05/10 17:44) |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| ===== Idris syntax ===== | ===== Idris syntax ===== | ||
| - | |||
| - | <code> | ||
| - | -- TOOD: Use different numbers, some that get larger and larger | ||
| - | |||
| - | y : Integer | ||
| - | y = 42 | ||
| - | |||
| - | --n: save and typecheck | ||
| - | |||
| - | k : Integer | ||
| - | k = -7 | ||
| - | |||
| - | --err k = someword | ||
| - | |||
| - | --REPL 2+3 | ||
| - | --REPL 1+1 | ||
| - | --REPL 1*0 | ||
| - | --REPL y | ||
| - | --REPL k | ||
| - | --REPL 2+y | ||
| - | --REPL y * k | ||
| - | --REPL k + y * k | ||
| - | --REPL -y | ||
| - | |||
| - | --REPL x -- not defined | ||
| - | |||
| - | --err y : Integer -- extra def | ||
| - | |||
| - | --err y = 8 -- extra def | ||
| - | |||
| - | --err y = 7 | ||
| - | |||
| - | --typecheck correctly and then REPL y | ||
| - | --type y=7, typecheck error, and then REPL y, it's gone | ||
| - | --'esc' to close info | ||
| - | |||
| - | --typecheck correctly and then REPL y | ||
| - | |||
| - | --u v : Interger | ||
| - | |||
| - | --err n = -103 | ||
| - | |||
| - | n : Integer | ||
| - | |||
| - | n2 : Integer | ||
| - | |||
| - | myFavoriteNumber : Integer | ||
| - | some_integer : Integer | ||
| - | |||
| - | n3 : Integer | ||
| - | --err n3 = 4.5 | ||
| - | |||
| - | --comment: | ||
| - | --42 is a popular number | ||
| - | --comment: | ||
| - | --I called this y because I did in the first video | ||
| - | |||
| - | --commant: | ||
| - | {- | ||
| - | this is the first video | ||
| - | where we use types | ||
| - | -} | ||
| - | |||
| - | --comment: | ||
| - | {- | ||
| - | Setting | ||
| - | n3 = 4.5 | ||
| - | doesn't work when n3 is an Integer | ||
| - | -} | ||
| - | |||
| - | m : Integer | ||
| - | |||
| - | willNotComeBackTo : Integer | ||
| - | |||
| - | --REPL willNotComeBackTo | ||
| - | --REPL willNotComeBackTo + 3 | ||
| - | |||
| - | n = 22 | ||
| - | |||
| - | --REPL n | ||
| - | |||
| - | e4hole : Integer | ||
| - | |||
| - | e4hole = ?will_complete_in_another_video | ||
| - | |||
| - | n' : Integer | ||
| - | n' = 33 | ||
| - | |||
| - | n_ : Integer | ||
| - | n_ = 44 | ||
| - | |||
| - | _n : Integer | ||
| - | _n = 55 | ||
| - | |||
| - | -- err .n : Integer | ||
| - | |||
| - | -- err n. : Integer | ||
| - | |||
| - | u : Integer | ||
| - | u = 2+5 | ||
| - | |||
| - | --REPL u | ||
| - | --REPL u+1 | ||
| - | |||
| - | v : Integer | ||
| - | v = n + 10 | ||
| - | |||
| - | --err |4 -- just wrting 4 | ||
| - | --err |=4 -- just wrting 4 | ||
| - | --err |hello -- just wrting hello | ||
| - | --err | 4 -- just wrting 4 | ||
| - | |||
| - | a : Integer | ||
| - | a | ||
| - | = 5000000 | ||
| - | |||
| - | --REPL a | ||
| - | |||
| - | --REPL | = 5000000 | ||
| - | |||
| - | b | ||
| - | : | ||
| - | Integer | ||
| - | b | ||
| - | = | ||
| - | 3000 | ||
| - | |||
| - | --REPL b | ||
| - | |||
| - | --err |3000 | ||
| - | |||
| - | |||
| - | msg : String | ||
| - | msg = "Hello" | ||
| - | |||
| - | youtube : String | ||
| - | youtube = "https://www.youtube.com" | ||
| - | |||
| - | --REPL youtube | ||
| - | |||
| - | --err msg = 3 | ||
| - | |||
| - | faulty : Integer | ||
| - | --err faulty = "you know what's gonna happen" | ||
| - | |||
| - | --REPL msg | ||
| - | --REPL youtube ++ msg | ||
| - | |||
| - | youtube_prefix : String | ||
| - | youtube_prefix = youtube ++ "/watch?v=" | ||
| - | |||
| - | episode2 : String | ||
| - | episode2 = youtube_prefix ++ "OGmwGSpwT1U" | ||
| - | |||
| - | editor : String | ||
| - | editor = "Atom" | ||
| - | |||
| - | blank : String | ||
| - | blank = " " | ||
| - | |||
| - | greeting : String | ||
| - | greeting = msg ++ blank ++ editor | ||
| - | |||
| - | --REPL "hello" ++ " my friend" | ||
| - | --err "hello" + " my friend" | ||
| - | --err 2 ++ 3 | ||
| - | --err 2 * "dear" | ||
| - | |||
| - | s3 : String | ||
| - | s3 = "check\nthis\nout" | ||
| - | |||
| - | warning : String | ||
| - | |||
| - | myword : String | ||
| - | |||
| - | --err myword : String | ||
| - | |||
| - | --err youword : Strings | ||
| - | |||
| - | --err someword : Madeup | ||
| - | |||
| - | --REPL String --n String : Type | ||
| - | |||
| - | ------ | ||
| - | |||
| - | -- Note that there are much more basic types defined. | ||
| - | -- We'll also define a lot of our own types. | ||
| - | |||
| - | -- Sometimes the REPL will tell us infomration | ||
| - | -- involving types we don't know yet. | ||
| - | -- Don't worry, we're gonna cover all the basics eventually. | ||
| - | |||
| - | -- Some more types beyond Integers, String, for example, | ||
| - | -- Bool, Double, Int, Nat, and then also some more complicated types like | ||
| - | -- List of Integers, or List of Strings, or List of Booleans. | ||
| - | -- And in languages like Haskell or Idris, we also have to do with | ||
| - | -- "type variables". This will be discussed soon. | ||
| - | |||
| - | ------ | ||
| - | |||
| - | f : Integer -> Integer | ||
| - | f x = x + 2000 | ||
| - | |||
| - | -- REPL f 7 | ||
| - | -- REPL z | ||
| - | -- REPL f z | ||
| - | -- REPL f (f z) | ||
| - | |||
| - | zplus : Integer | ||
| - | zplus = f z | ||
| - | |||
| - | -------- | ||
| - | |||
| - | --load in terminal repl | ||
| - | --explain 'it' | ||
| - | |||
| - | --explain :r | ||
| - | --explain :l | ||
| - | |||
| - | </code> | ||
| - | |||
| | [[Idris]] $\blacktriangleright$ Idris syntax $\blacktriangleright$ [[...]] | | | [[Idris]] $\blacktriangleright$ Idris syntax $\blacktriangleright$ [[...]] | | ||
| ==== Note ==== | ==== Note ==== | ||
