Warning: this is an htmlized version!
The original is across this link,
and the conversion rules are here.
-- This file: 
--   http://angg.twu.net/IDRIS/Tut.idr.html
--   http://angg.twu.net/IDRIS/Tut.idr
--           (find-angg "IDRIS/Tut.idr")
--
-- This is my eev-ized version of the Idris tutorial. See:
--   http://angg.twu.net/emacsconf2019.html <- eev @ EmacsConf 2019
--   http://angg.twu.net/#eev
--   (find-eev-quick-intro)
--
-- To install Idris on Debian, follow these instructions:
--   (find-es "idris" "idris-on-debian")
-- and add ~/.cabal/bin to the PATH:
--   (find-es "haskell" "cabal-PATH")
--
-- To download Idris from git and compile its documentation into PDFs, do:
--   (find-es "idris" "idris-git")
--   (find-es "idris" "idris-git" "make user_doc_pdf")
-- We will get a file "idris-documentation-complete.pdf".
-- Here's how I use it:
--   (find-pdf-like-intro)
--   (find-angg ".emacs" "idris")
--   (find-es "idris" "idris-doc-complete")
-- See also:
--   (find-es "idris" "idris-docs-online")
--
-- To install idris-mode for Emacs and also download it from git:
--   (find-es "idris" "idris-mode-git")
-- Its main keys (IMHO) are `C-c C-l' and `C-c C-t':
--   https://github.com/idris-hackers/idris-mode
--   (find-idrismodegitfile "readme.markdown" "C-c C-l")
--   (find-idrismodegitfile "readme.markdown" "C-c C-t")
--
-- Note: I know VERY LITTLE Idris at the moment! See:
--   http://angg.twu.net/math-b.html#notes-yoneda
--             (find-TH "math-b"    "notes-yoneda")



-- «.import»			(to "import")
-- «.types-and-functions»	(to "types-and-functions")
--   «.data-types»		(to "data-types")
--   «.functions»		(to "functions")
--   «.dependent-types»		(to "dependent-types")
--   «.useful-data-types»	(to "useful-data-types")
--     «.records»		(to "records")
--   «.more-expressions»	(to "more-expressions")
--   «.interfaces»		(to "interfaces")
-- «.theorem-proving»		(to "theorem-proving")
--
-- «.Pair»			(to "Pair")



-- «import»  (to ".import")
-- (find-es "idris" "import")
import public Data.Vect



-- «types-and-functions»  (to ".types-and-functions")
-- (find-idrisdoccpage (+ 1 4) "1.3      Types and Functions")
-- (find-idrisdocctext (+ 1 4) "1.3      Types and Functions")
-- (find-idrisdoccpage (+ 1 4) "1.3.1    Primitive Types")
-- (find-idrisdocctext (+ 1 4) "1.3.1    Primitive Types")

-- «data-types»  (to ".data-types")
-- (find-idrisdoccpage (+ 1 5) "1.3.2      Data Types")
-- (find-idrisdocctext (+ 1 5) "1.3.2      Data Types")
-- (find-idrisdoccpage (+ 1 172) "Data types")
-- (find-idrisdocctext (+ 1 172) "Data types")

data MyNat    = Z   | S MyNat           -- Natural numbers
data MyList a = Nil | (::) a (MyList a) -- Polymorphic lists

{-
* (eepitch-to-buffer "*idris-repl*")
MyNat
Z
-- Can't disambiguate name: Main.Z, Prelude.Nat.Z
-- (find-idrisdoccpage (+ 1 221) "6.20.2     Namespaces and type-directed disambiguation")
-- (find-idrisdocctext (+ 1 221) "6.20.2     Namespaces and type-directed disambiguation")

-}


-- «functions»  (to ".functions")
-- (find-idrisdoccpage (+ 1 6) "1.3.3    Functions")
-- (find-idrisdocctext (+ 1 6) "1.3.3    Functions")

-- Unary addition
myplus : Nat -> Nat -> Nat
myplus Z     y = y
myplus (S k) y = S (myplus k y)

-- Unary multiplication
mymult : Nat -> Nat -> Nat
mymult Z     y = Z
mymult (S k) y = myplus y (mymult k y)


{-
* (eepitch-to-buffer "*idris-repl*")
myplus (S (S Z)) (S (S Z))
mymult (S (S (S Z))) (myplus (S (S Z)) (S (S Z)))
(S (S (S (S Z))))
myplus 2 2
mymult 3 (myplus 2 2)

-}

-- (find-idrisdoccpage (+ 1 7) "where clauses")
-- (find-idrisdocctext (+ 1 7) "where clauses")

reverse : List a -> List a
reverse xs = revAcc [] xs where
  revAcc : List a -> List a -> List a
  revAcc acc [] = acc
  revAcc acc (x :: xs) = revAcc (x :: acc) xs

{-
* (eepitch-to-buffer "*idris-repl*")
[2, 3, 4]
reverse [2, 3, 4]

-}

-- (find-idrisdoccpage (+ 1 7) "Note: Scope")
-- (find-idrisdocctext (+ 1 7) "Note: Scope")

foo : Int -> Int
foo x = case isLT of
            Yes => x*2
            No => x*4
    where
       data MyLT = Yes | No

       isLT : MyLT
       isLT = if x < 20 then Yes else No

{-
* (eepitch-to-buffer "*idris-repl*")
foo 19   --> 38
foo 20   --> 80

-}



-- «dependent-types»  (to ".dependent-types")
-- (find-idrisdoccpage (+ 1 8) "1.3.4     Dependent Types")
-- (find-idrisdocctext (+ 1 8) "1.3.4     Dependent Types")
-- (find-idrisdoccpage (+ 1 9) "Vectors")
-- (find-idrisdocctext (+ 1 9) "Vectors")
-- (find-idrisgitfile "libs/base/Data/Vect.idr" "data Vect :")

isSingleton : Bool -> Type
isSingleton True = Nat
isSingleton False = List Nat

mkSingle : (x : Bool) -> isSingleton x
mkSingle True = 0
mkSingle False = []

ssum : (single : Bool) -> isSingleton single -> Nat
ssum True x = x
ssum False [] = 0
ssum False (x :: xs) = x + ssum False xs

-- (find-idrisdoccpage (+ 1 11) "\"using\" notation")
-- (find-idrisdocctext (+ 1 11) "\"using\" notation")

data IsElem : a -> Vect n a -> Type where
   Here : {x:a} ->    {xs:Vect n a} -> IsElem x (x :: xs)
   There : {x,y:a} -> {xs:Vect n a} -> IsElem x xs -> IsElem x (y :: xs)

{-
* (eepitch-to-buffer "*idris-repl*")
Vect 4 Nat
Vect
IsElem
:t IsElem
IsElem Nat

3 :: 4 :: Nil
[3, 4]

IsElem [3, 4]

-}


-- testVec : Vect 4 Int
-- testVec = 3 :: 4 :: 5 :: 6 :: Nil

-- inVect : IsElem 5 Main.testVec
-- inVect = There (There Here)

-- (find-idrisdoccpage (+ 1 12) "1.3.5    I/O")
-- (find-idrisdocctext (+ 1 12) "1.3.5    I/O")
-- (find-idrisdoccpage (+ 1 12) "1.3.6    \"do\" notation")
-- (find-idrisdocctext (+ 1 12) "1.3.6    \"do\" notation")
-- (find-idrisdoccpage (+ 1 13) "1.3.7    Laziness")
-- (find-idrisdocctext (+ 1 13) "1.3.7    Laziness")
-- (find-idrisdoccpage (+ 1 13) "1.3.8    Codata Types")
-- (find-idrisdocctext (+ 1 13) "1.3.8    Codata Types")




-- «useful-data-types»  (to ".useful-data-types")
-- (find-idrisdoccpage (+ 1 14) "1.3.9    Useful Data Types")
-- (find-idrisdocctext (+ 1 14) "1.3.9    Useful Data Types")
-- (find-idrisdoccpage (+ 1 15)   "List and Vect")
-- (find-idrisdocctext (+ 1 15)   "List and Vect")
-- (find-idrisdocctext (+ 1 15)   "List and Vect" "[1,2,3] means")
-- (find-idrisdoccpage (+ 1 15) "  Aside: Anonymous functions and operator sections")
-- (find-idrisdocctext (+ 1 15)   "Aside: Anonymous functions and operator sections")
-- (find-idrisdocctext (+ 1 15)   "Aside: Anonymous functions and operator sections" "=>")
-- (find-idrisdoccpage (+ 1 17)   "Dependent Pairs")
-- (find-idrisdocctext (+ 1 17)   "Dependent Pairs")
-- (find-idrisdoccpage (+ 1 17)     "vec : (n : Nat ** Vect n Int)")
-- (find-idrisdocctext (+ 1 17)     "vec : (n : Nat ** Vect n Int)")
-- (find-idrisdoccpage (+ 1 17)     "with (filter p xs)" "|")
-- (find-idrisdocctext (+ 1 17)     "with (filter p xs)" "|")
-- (find-idrisdoccpage (+ 1 17)   "Records")
-- (find-idrisdocctext (+ 1 17)   "Records")
-- (find-idrisdoccpage (+ 1 19)   "Dependent Records")
-- (find-idrisdocctext (+ 1 19)   "Dependent Records")

-- «records»  (to ".records")
-- (find-idrisdoccpage (+ 1 17)   "Records")
-- (find-idrisdocctext (+ 1 17)   "Records")

record Person where
    constructor MkPerson
    firstName, middleName, lastName : String
    age : Int

fred : Person
fred = MkPerson "Fred" "Joe" "Bloggs" 30

{-
* (eepitch-to-buffer "*idris-repl*")
fred
firstName fred
age fred
:t firstName
record { firstName = "Jim" } fred
record { firstName = "Jim", age $= (+ 1) } fred

-}




-- (find-idrisgitfile "libs/prelude/Prelude.idr")
-- (find-idrisgitfile "libs/prelude/Prelude/List.idr")
-- (find-idrisgitfile "libs/base/Data/List.idr")

-- (find-idrisgitfile "libs/prelude/Prelude/")
-- (find-idrisgitfile "libs/prelude/Prelude/Bool.idr")
-- (find-idrisgitfile "libs/prelude/Prelude/Either.idr")
-- (find-idrisgitfile "libs/prelude/Builtins.idr" "data Pair :")
-- (find-idrisgitfile "libs/prelude/Builtins.idr" "data DPair :")
-- (find-idrisgitgrep "grep --color -nrH -e impossible libs/")
-- (find-idrisgitgrep "grep --color -nrH -e postulate libs/")
-- (find-idrisgitgrep "grep --color -nrH -e Vect libs/")

-- (find-idrisdoccpage (+ 1 179) "LinearTypes")
-- (find-idrisdocctext (+ 1 179) "LinearTypes")






-- «more-expressions»  (to ".more-expressions")
-- (find-idrisdoccpage (+ 1 19) "1.3.10    More Expressions")
-- (find-idrisdocctext (+ 1 19) "1.3.10    More Expressions")
-- (find-idrisdoccpage (+ 1 19)   "let bindings")
-- (find-idrisdocctext (+ 1 19)   "let bindings")
-- (find-idrisdoccpage (+ 1 20)   "List comprehensions" "[ expression | qualifiers ]")
-- (find-idrisdocctext (+ 1 20)   "List comprehensions" "[ expression | qualifiers ]")
-- (find-idrisdoccpage (+ 1 20)   "case expressions")
-- (find-idrisdocctext (+ 1 20)   "case expressions")
-- (find-idrisdocctext (+ 1 20)   "case expressions" "(== c)")
-- (find-idrisdoccpage (+ 1 21) "1.3.11     Totality")
-- (find-idrisdocctext (+ 1 21) "1.3.11     Totality")



-- «interfaces»  (to ".interfaces")
-- (find-idrisdoccpage (+ 1 21) "1.4      Interfaces")
-- (find-idrisdocctext (+ 1 21) "1.4      Interfaces")
-- (find-idrisdoccpage (+ 1 22) "1.4.1    Default Definitions")
-- (find-idrisdocctext (+ 1 22) "1.4.1    Default Definitions")
-- (find-idrisdoccpage (+ 1 22) "1.4.2    Extending Interfaces")
-- (find-idrisdocctext (+ 1 22) "1.4.2    Extending Interfaces")
-- (find-idrisdoccpage (+ 1 23)   "multiple constraints")
-- (find-idrisdocctext (+ 1 23)   "multiple constraints")
-- (find-idrisdoccpage (+ 1 23) "1.4.3    Functors and Applicatives")
-- (find-idrisdocctext (+ 1 23) "1.4.3    Functors and Applicatives")
-- (find-idrisdoccpage (+ 1 23) "1.4.4    Monads and do-notation")
-- (find-idrisdocctext (+ 1 23) "1.4.4    Monads and do-notation")
-- (find-idrisdoccpage (+ 1 25)   "do Just x_ok <- readNumber |")
-- (find-idrisdocctext (+ 1 25)   "do Just x_ok <- readNumber |")
-- (find-idrisdoccpage (+ 1 25)   "Monad comprehensions")
-- (find-idrisdocctext (+ 1 25)   "Monad comprehensions")

-- (find-idrisdoccpage (+ 1 39) "filter   p (x :: xs) |")
-- (find-idrisdocctext (+ 1 39) "filter   p (x :: xs) |")
-- (find-idrisdoccpage (+ 1 39) "with clause, followed by a vertical bar |")
-- (find-idrisdocctext (+ 1 39) "with clause, followed by a vertical bar |")


-- (find-idrisdoccpage (+ 1 173) "Records")
-- (find-idrisdocctext (+ 1 173) "Records")




-- «theorem-proving»  (to ".theorem-proving")
-- (find-idrisdoccpage (+ 1 40) "1.9     Theorem Proving")
-- (find-idrisdocctext (+ 1 40) "1.9     Theorem Proving")
-- (find-idrisdoccpage (+ 1 40) "1.9.1    Equality")
-- (find-idrisdocctext (+ 1 40) "1.9.1    Equality")
-- (find-idrisdoccpage (+ 1 41) "1.9.2    The Empty Type")
-- (find-idrisdocctext (+ 1 41) "1.9.2    The Empty Type")
-- (find-idrisdoccpage (+ 1 41) "1.9.3    Simple Theorems")
-- (find-idrisdocctext (+ 1 41) "1.9.3    Simple Theorems")

-- plusReduces : (n:Nat) -> plus Z n = n

plusReducesZ : (n:Nat) -> n = plus n Z
plusReducesZ Z = Refl
plusReducesZ (S k) = cong (plusReducesZ k)

-- cong : {f : t -> u} -> a = b -> f a = f b

plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)
plusReducesS Z m = Refl
plusReducesS (S k) m = cong (plusReducesS k m)

{-
* (eepitch-to-buffer "*idris-repl*")
plusReducesZ 3
plusReducesS 3 4
3 = 3
3 = 4
Refl
Refl 3
Refl Nat
impossible

-}

-- (find-idrisdoccpage (+ 1 42) "1.9.4    Theorems in Practice")
-- (find-idrisdocctext (+ 1 42) "1.9.4    Theorems in Practice")

-- parity : (n:Nat) -> Parity n
-- parity Z     = Even {n=Z}
-- parity (S Z) = Odd {n=Z}
-- parity (S (S k)) with (parity k)
--   parity (S (S (j + j)))     | Even = Even {n=S j}
--   parity (S (S (S (j + j)))) | Odd = Odd {n=S j}


-- Unfortunately, this fails with a type error:
-- 
-- When checking right hand side of with block in views.parity with expected type
--         Parity (S (S (j + j)))
-- 
-- Type mismatch between
--         Parity (S j + S j) (Type of Even)
-- and
--         Parity (S (S (plus j j))) (Expected type)



-- (find-idrisdoccpage (+ 1 45) "1.10      Provisional Definitions")
-- (find-idrisdocctext (+ 1 45) "1.10      Provisional Definitions")
-- (find-idrisdoccpage (+ 1 48) "1.10.2     Suspension of Disbelief")
-- (find-idrisdocctext (+ 1 48) "1.10.2     Suspension of Disbelief")

-- (find-idrisdoccpage (+ 1 55) "1.13.1    Implicit arguments")
-- (find-idrisdocctext (+ 1 55) "1.13.1    Implicit arguments")

-- (find-books "__logic/__logic.el" "hindley-seldin2")
-- (find-hindleyseldin2page (+ 14  61)  "4D Abstract numerals and Z")

-- (find-idrisdoccpage (+ 1 135) "5.2     Curry-Howard correspondence")
-- (find-idrisdocctext (+ 1 135) "5.2     Curry-Howard correspondence")
-- (find-idrisdoccpage (+ 1 135)   "the (1=1) Refl")
-- (find-idrisdocctext (+ 1 135)   "the (1=1) Refl")
-- (find-idrisdoccpage (+ 1 136) "5.2.1      And (conjunction)")
-- (find-idrisdocctext (+ 1 136) "5.2.1      And (conjunction)")
-- (find-idrisdoccpage (+ 1 136) "5.2.2      Or (disjunction)")
-- (find-idrisdocctext (+ 1 136) "5.2.2      Or (disjunction)")
-- (find-idrisdoccpage (+ 1 137) "``postulate``")
-- (find-idrisdocctext (+ 1 137) "``postulate``")

{-
* (eepitch-to-buffer "*idris-repl*")
2 = 2
3 = 4
Refl                -- err
:t Refl
the (2 = 2)
the (2 = 2) Refl
the (3 = 4)
the (3 = 4) Refl    -- err

Pair
Pair Nat Nat
Either Nat Int
Int
Bool

-}



-- (find-fline "~/IDRIS/Yoneda.idr")

-- (find-idrisgitfile "libs/prelude/Builtins.idr" "data Pair :")

-- proo : (P, Q, R : Type)  -> Type
-- proo : (p, q, r : Type)  -> Type
proo : Type -> Type -> Type -> Type
proo p q r = (Pair p q) -> r
-- proo = ?proo
-- proo p q r = Nat


-- (find-idrisdoccpage (+ 1 179) "| Impossible")
-- (find-idrisdocctext (+ 1 179) "| Impossible")

{-
* (eepitch-to-buffer "*idris-repl*")
proo
Nat
AndIntro

the Integer -3
the Nat -3

MkPair 

-}



-- «Pair»  (to ".Pair")