Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Last revision Both sides next revision
idris_syntax [2016/05/10 17:44]
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 ====
Link to graph
Log In
Improvements of the human condition
limeGraphxioms