david-christiansen

module HList

%default total

data HList : List Type -> Type where
  (::) : t -> (xs : HList ts) -> HList (t :: ts)
  Nil : HList []

foo : HList [Int, String, Int]
foo = [3, "yes", 17]

david-christiansen

module PropDemo

data GreaterThanTwo : Nat -> Type where
  threeOK : GreaterThanTwo 3
  moreOK : GreaterThanTwo n -> GreaterThanTwo (S n)

total sumGreater : GreaterThanTwo n -> GreaterThanTwo m -> GreaterThanTwo (n + m)
sumGreater threeOK mOK = moreOK (moreOK (moreOK mOK))
sumGreater (moreOK nOK') mOK = moreOK (sumGreater nOK' mOK)

david-christiansen

module Lambda

%default total

infixr 8 ==>

data T : Type where
  U : T
  NAT : T
  (*) : T -> T -> T

david-christiansen

module Addition


class Plus (n : Nat) (m : Nat) (o : Nat) where {}

instance Plus Z m m where {}

instance Plus n m o => Plus (S n) m (S o) where {}

parameters (n : Nat, m : Nat)

david-christiansen

module Bugfind



import Language.Reflection
import Language.Reflection.Util

foo : TT
foo = Erased

david-christiansen

module JSON

import Data.HVect

import Control.Monad.Identity

import Lightyear.Core
import Lightyear.Combinators
import Lightyear.Strings

david-christiansen

module PreOrderReasoning


-- QED is first to get the precedence to work out. It's just refl with an explicit argument.
syntax [expr] "QED" = qed expr
-- foo ={ prf }= bar ={ prf' }= fnord QED
-- is a proof that foo is related to fnord, with the intermediate step being bar, justified by prf and prf'
syntax [from] "={" [prf] "}=" [to] = step from prf to

--These are the components for using the syntax with equality

david-christiansen

drc@drc:~/Documents/Code/Idris/error-reflection-test$ idris ErrorTest.idr
     ____    __     _                                          
    /  _/___/ /____(_)____                                     
    / // __  / ___/ / ___/     Version 0.9.10.1-git:5361547
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/      
 /___/\__,_/_/  /_/____/       Type :? for help                

Type checking ./ErrorTest.idr
*ErrorTest> the Nat ""
ERROR HAPPENED!

david-christiansen

module ErrorTest

import Language.Reflection
import Language.Reflection.Errors
import Language.Reflection.Utils

%language ErrorReflection

data Ty = TUnit | TFun Ty Ty

david-christiansen

import Language.Reflection.Errors
import Language.Reflection.Utils

%language ErrorReflection

total
cadr :  (xs : List a)
     -> {auto cons1 : isCons xs = True}
     -> {auto cons2 : isCons (tail xs cons1) = True}
     -> a