edwinb

  using (xs : List a)
    data InBound : Nat -> List a -> Set where
         inO : InBound O (x :: xs)
         inS : InBound k xs -> InBound (S k) (x :: xs)

edwinb

  -- Idris type classes actually take any kind of value as a parameter,
  -- we're not restricted to Sets or parameterised Sets.
  
  -- So we actually have 'value classes'. It seems we can use type class
  -- resolution to make rudimentary decision procedures, then:
  
  using (xs : List a)
    data Elem : a -> List a -> Set where
         Here  : Elem x (x :: xs)
         There : Elem x xs -> Elem x (y :: xs)

edwinb

  data Succ : Nat -> Set where
       yes : Succ (S k)
  
  data RationalP = RatP Nat Nat
  
  data Rational : Set where
       Rat : (num : Nat) -> (den : Nat) -> Succ den -> Rational
  
  total toRational : RationalP -> Rational
  toRational (RatP x y) = Rat x (S y) yes

edwinb

-- Not fine:

  mergeBy : (a -> a -> Ordering) -> List a -> List a -> List a
  mergeBy order []      right   = right
  mergeBy order left    []      = left
  mergeBy order (x::xs) (y::ys) =
    case order x y of
      LT => x :: mergeBy order xs (y :: ys)
      _  => y :: mergeBy order (x :: xs) ys

edwinb

  plus_comm : (n : Nat) -> (m : Nat) -> n + m = m + n 
   
  -- Base case 
  (O + m = m + O) <== plus_comm =  
      rewrite ((m + O = m) <== plusZeroRightNeutral) ==> (m = m) in refl 
   
  -- Step case 
  (S k + m = m + S k) <== plus_comm = 
      rewrite ((k + m = m + k) <== plus_comm) ==> (S (m + k) = m + S k) in 
      rewrite ((S (m + k) = m + S k) <== plusSuccRightSucc) in 

edwinb

plus_comm : (n : Nat) -> (m : Nat) -> (n + m = m + n)

-- Base case
(O + m = m + O) <== plus_comm = 
    rewrite ((m + O = m) <== plusZeroRightNeutral) ==> 
            (O + m = m) in refl

-- Step case
(S k + m = m + S k) <== plus_comm =
    rewrite ((k + m = m + k) <== plus_comm) in

edwinb

module Reflect

import Decidable.Equality

using (xs : List a, ys : List a, G : List (List a))

  data Elem : a -> List a -> Type where
       Stop : Elem x (x :: xs)
       Pop  : Elem x ys -> Elem x (y :: xs)

edwinb

Stream.idr:39:9:Incomplete term Effects.>>= {m = IO} {a = PID} {xs =
Prelude.List.:: {a = EFFECT} (MkEff (ProtoT {a = Actions} {p = Type} {chan =
PID} (DoSend {princ = Type} (Symbol_ "Server") Command (\ t : Command =>
mkProcess {princ = Type} {t = ()} {xs = Prelude.List.:: {a = Type} (Symbol_
"Client") (Prelude.List.:: {a = Type} (Symbol_ "Server") (Prelude.List.Nil {a =
Type}))} (Symbol_ "Client") (case block in count 0 t t) (\ x : () => End)))
(Prelude.List.Nil {a = (Type, PID)})) (Msg Type PID)) (Prelude.List.:: {a =
EFFECT} (MkEff () Conc) (Prelude.List.:: {a = EFFECT} (MkEff () StdIO)
(Prelude.List.Nil {a = EFFECT})))} {xs' = \ v : PID => updateWith {a = EFFECT}
{ys = Prelude.List.:: {a = EFFECT} (MkEff () Conc) (Prelude.List.Nil {a =

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
  

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