edwinb

  record Person : Nat -> Type where
         MkPerson : (name : String) ->
                    (age : Nat) ->
                    Person age
  
  record Event : Type where
         MkEvent : (name : String) -> (organiser : Person a) -> Event
  
  record Meeting : Int -> Type where
         MkMeeting : (event : Event) ->

edwinb

-- We could define the relation like this:

data LessThan : Nat -> Nat -> Type where
     LT_Z : LessThan Z (S m)
     LT_S : LessThan n m -> LessThan (S n) (S m)

-- Then calculate a proof, if one exists:
  
isLessThan : (m : Nat) -> (n : Nat) -> Maybe (LessThan m n)
isLessThan Z Z = Nothing

edwinb

@article{JFP:9060502,
author = {BRADY,EDWIN},
title = {Idris, a general-purpose dependently typed programming language: Design and implementation},
journal = {Journal of Functional Programming},
volume = {23},
issue = {05},
month = {9},
year = {2013},
issn = {1469-7653},
pages = {552--593},

edwinb

Keybase proof

I hereby claim:

• I am edwinb on github.
• I am edwinb (https://keybase.io/edwinb) on keybase.
• I have a public key whose fingerprint is 9FDE 3D18 203F 0CFA DD7A A817 F219 A102 9E17 61E3

To claim this, I am signing this object:

edwinb

foo : (xs : Vect n a) -> (ys : Vect m a) -> ?noIdea
foo xs ys = xs ++ ys

Currently this gives:

Can't unify
        Vect (n + m) a
with
        ?noIdea

edwinb

class Marshal val chan where
      sendType : Type -> Type
      recvType : Type -> Type

      marshal   : val -> sendType val
      unmarshal : sendType val -> recvType val

edwinb

(./DB/SQLite/SQLiteNew.idr:19:13,"Type\n")
(./DB/SQLite/SQLiteNew.idr:19:13,"Type\n")
(./DB/SQLite/SQLiteNew.idr:20:13,"List (List DBVal)\n")
(./DB/SQLite/SQLiteNew.idr:20:19,"List DBVal)\n")
(./DB/SQLite/SQLiteNew.idr:22:10,"Type\n")
(./DB/SQLite/SQLiteNew.idr:22:10,"Type\n")
(./DB/SQLite/SQLiteNew.idr:23:10,"String\n")
(./DB/SQLite/SQLiteNew.idr:25:15,"Type\n")
(./DB/SQLite/SQLiteNew.idr:25:15,"Type\n")
(./DB/SQLite/SQLiteNew.idr:26:15,"String\n")

edwinb

Ran ffi001...FAILURE
2c2
< 0.9995736030415051 : Float
---
0.9995736030415051 : Float
make[1]: *** [ffi001.test] Error 1

edwinb

Problem:
--------

You tried to use the random number generator effect when it wasn't available.

New error message:
------------------

Expr.idr:31:6:When elaborating right hand side of eval:
Can't solve goal 

edwinb

  module erase
  
  data LessThan : Nat -> Nat -> Type where
       LtO : LessThan Z (S k)
       LtS : LessThan x y -> LessThan (S x) (S y)
  
  minus : (x : Nat) -> (y : Nat) -> LessThan y x -> Nat
  minus (S k) Z LtO = S k
  minus (S k) (S j) (LtS z) = minus k j