Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision 		Previous revision
Last revision Both sides next revision
idris_syntax [2016/05/10 17:36]
nikolaj 		idris_syntax [2017/06/06 13:07]
nikolaj
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 ====
-I'll try to take all the primitive notions and write down 1 example with them, respectively.+I'll try to take all the primitive notions and write down one example with them, respectively.
  
 This list largely overlaps with [[Haskell]]. This list largely overlaps with [[Haskell]].
- 
-> 
->Todo: 
-> 
->Draw some neat images (and find some quite place...) 
-> 
  
 == Defining types == == Defining types ==
Link to graph
Log In
Improvements of the human condition
limeGraphxioms