This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Lambda | |
%default total | |
infixr 8 ==> | |
data T : Type where | |
U : T | |
NAT : T | |
(*) : T -> T -> T |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Bugfind | |
import Language.Reflection | |
import Language.Reflection.Util | |
foo : TT | |
foo = Erased |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module JSON | |
import Data.HVect | |
import Control.Monad.Identity | |
import Lightyear.Core | |
import Lightyear.Combinators | |
import Lightyear.Strings |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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! |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module ErrorTest | |
import Language.Reflection | |
import Language.Reflection.Errors | |
import Language.Reflection.Utils | |
%language ErrorReflection | |
data Ty = TUnit | TFun Ty Ty |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
OlderNewer