Skip to content

Instantly share code, notes, and snippets.

Avatar

David Thrane Christiansen david-christiansen

View GitHub Profile
View gist:4994451
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]
View gist:4994631
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
david-christiansen / Lambda.idr
Created Jul 29, 2013
Error with idiom brackets in equality type
View Lambda.idr
module Lambda
%default total
infixr 8 ==>
data T : Type where
U : T
NAT : T
(*) : T -> T -> T
@david-christiansen
david-christiansen / Addition.idr
Created Aug 2, 2013
Using type classes for logic programming
View Addition.idr
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)
View Bugfind.idr
module Bugfind
import Language.Reflection
import Language.Reflection.Util
foo : TT
foo = Erased
@david-christiansen
david-christiansen / JSON.idr
Created Dec 10, 2013
Zygote of a JSON parser
View JSON.idr
module JSON
import Data.HVect
import Control.Monad.Identity
import Lightyear.Core
import Lightyear.Combinators
import Lightyear.Strings
@david-christiansen
david-christiansen / PreorderReasoning.idr
Created Dec 14, 2013
Agda-style preorder reasoning in Idris
View PreorderReasoning.idr
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
david-christiansen / gist:8336956
Created Jan 9, 2014
First reflected error in Idris
View gist:8336956
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
david-christiansen / ErrorTest.idr
Created Jan 10, 2014
First-ever Idris DSL with domain-specific error messages!
View ErrorTest.idr
module ErrorTest
import Language.Reflection
import Language.Reflection.Errors
import Language.Reflection.Utils
%language ErrorReflection
data Ty = TUnit | TFun Ty Ty
@david-christiansen
david-christiansen / FunErrTest.idr
Created Jan 23, 2014
Error reflection now supports specific function arguments
View FunErrTest.idr
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
You can’t perform that action at this time.