Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
idris_syntax [2017/06/06 13:07]
nikolaj
idris_syntax [2017/06/06 13:08] (current)
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 ====
Link to graph
Log In
Improvements of the human condition