lmarburger

$ ruby-parse -E -e 'def a(*) end
a = 1
a(:a)
a :a'
def a(*) end
^~~ kDEF "def"                                  expr_fname   [0 <= cond] [0 <= cmdarg]
def a(*) end
    ^ tIDENTIFIER "a"                           expr_endfn   [0 <= cond] [0 <= cmdarg]
def a(*) end
     ^ tLPAREN2 "("                             expr_beg     [0 <= cond] [0 <= cmdarg]

lmarburger

$x = 0
h = Hash.new {|h, k| h[k] = $x += 1 }
p h[:a]
p h[:a]
p h[:b]
p h

$y = 0
i = Hash.new { $y += 1 }
p i[:a]

lmarburger

$x = 0
h = Hash.new {|h, k| h[k] = $x += 1 }
p h[:a]
p h[:a]
p h[:b]
p h

$y = 0
i = Hash.new { $y += 1 }
p i[:a]

lmarburger

$ ruby -v
ruby 1.9.3p545 (2014-02-24 revision 45159) [x86_64-darwin13.1.0]

$ rbenv exec travis --version
rbenv: travis: command not found

The `travis' command exists in these Ruby versions:
  2.1.1

$ which travis

lmarburger

class Outer
  A = 'outer'
end
puts Outer::A  #=> outer

class Outer
  class Inner
    puts A  #=> outer
  end
end

lmarburger

module lec1

total
ltake : Nat -> List a -> List a
ltake Z     _         = []
ltake _     []        = []
ltake (S k) (x :: xs) = x :: (ltake k xs)

-- > ltake 1 []
-- (input):0:0:Incomplete term ltake (fromInteger 1) []

lmarburger

{-
  From the Prelude: https://github.com/idris-lang/Idris-dev/blob/master/libs/prelude/Prelude/Bool.idr#L18-L27
  data so : Bool -> Type where oh : so True
-}

-- Type checks fine
passTest : so (1 < 2)
passTest = oh

-- Fails to type check

lmarburger

data Expr = Var String
          | Val Int
          | Add Expr Expr
          | Let (List (String, Int)) Expr

data Eval : Type -> Type where
  MkEval : (List (String, Int) -> Maybe a) -> Eval a

fetch : String -> Eval Int
fetch x = MkEval (\e => fetchVal e) where

lmarburger

data Expr = Var String
          | Val Int
          | Add Expr Expr

data Eval : Type -> Type where
  MkEval : (List (String, Int) -> Maybe a) -> Eval a

fetch : String -> Eval Int
fetch x = MkEval (\e => fetchVal e) where
  fetchVal : List (String, Int) -> Maybe Int

lmarburger

even : Nat -> Bool
even Z = True
even (S k) = odd k where
  odd Z = False
  odd (S k) = even k

/*
*even> even 0
True : Bool
*even> even 1