git.iko.soy/Idris-dev
on master help sign in
history ofsrc/Idris/Reflection.hs
all commits
bd3929fFix small typoBrian Wignall cc7ef9aRemove old eliminator generation and induction tactic (#4351)Ahmad Salim Al-Sibahi 3ccb494Remove the empty property 'copyright'.Jan de Muijnck-Hughes f984657Merge pull request #4093 from melted/export_listsNiklas Larsson 4a3fe0cLinearTypes extension improvementsEdwin Brady c38dc74Add export lis t to Idris.ReflectionNiklas Larsson c4ac8cbDrop support for GHC <= 7.10.3Thomas Scholtes fb185aaCheck for linearity of constructorsEdwin Brady a5033e7Add linear LamEdwin Brady e1c210bAdd 'RigCount' to Pi and PVarEdwin Brady e3daf28Add RigCount to environmentEdwin Brady ea88b5eBetter choice of pattern to inspect in coverageEdwin Brady e6ceb5cAlphabetize and indent imports and LANGUAGE pragmasEcho Nolan 0df1270Change Instance to implementation (#3404)(λ _ λ) 08cef17HLint DIrected Code CleanupJan de Muijnck-Hughes fc3e88cMerge branch 'master' of github.com:idris-lang/Idris-devEdwin Brady fdfa04cStore file with constraints + exportEdwin Brady be093dcAdded more context to the no rewriting error, to include terms being rewritten withAhmad Salim Al-Sibahi 0896073Added documentation for modules.Jan de Muijnck-Hughes eaf5211Add the ability to define datatypes in ElabDavid Raymond Christiansen 1cf8fe9Context for "Can't find implementation"Edwin Brady bd26521Fix reflection of NativeTy valuesMelvar Chen 1527899Merge branch 'elab-lookup-function-def' of https://github.com/shlevy/Idris-dev into shlevy-elab-lookup-function-defDavid Raymond Christiansen 9f3675aStore patvar binding types in idris_patdefsShea Levy 39d643bMerge branch 'elab-lookup-function-def' of https://github.com/shlevy/Idris-dev into shlevy-elab-lookup-function-defDavid Raymond Christiansen cdc7238Make FunDefn and FunClause polymorphic over TT and RawShea Levy 42eeb6eUpdate reflection for Float -> Double changeDavid Raymond Christiansen c1fabb1Implement LookupFunDefnShea Levy f7e1990Add lookup of FunArgs for global names to ElabDavid Raymond Christiansen 0f89577Remove NErasedDavid Raymond Christiansen d5b66a9Show source location of case block namesDavid Raymond Christiansen b774d12Remove NLet binder from reflection APIDavid Raymond Christiansen 105c230Simplify reflection and RawDavid Raymond Christiansen 7dde291fix GHC 7.10 compilation warningDmitry Bushev d952c94Improve error message when reifying non-constantDavid Raymond Christiansen 766b73aLook up operator fixity in ElabDavid Raymond Christiansen 763ac00Merge remote-tracking branch 'upstream/master' into wip/tacticalDavid Raymond Christiansen 7095d6cProof search should only use user visible namesEdwin Brady 56869f6Properly reify reflected character constantsDavid Raymond Christiansen d54064fEvaluator access in Elab scriptsDavid Raymond Christiansen 3b90559Indicate constructor fields vs parameters in ElabDavid Raymond Christiansen cf9f36bFix copy-paste bug when reifying reflected tacticsBrian Koropoff 012b898Fix quasiquotes of Raw bindingsDavid Raymond Christiansen ff60396Make apply match internal behaviourDavid Raymond Christiansen b2dc1fcAdd missing reflection constructorDavid Raymond Christiansen 124074aAdd erasure info to Elab reflectionDavid Raymond Christiansen 4ede52dAllow the pretty-printing of Raw termsDavid Raymond Christiansen 1054d7dAdd UnknownImplicit errorEdwin Brady a95debfFix reflection of special namesDavid Raymond Christiansen 8ab1ac6Richer universe error objectsDavid Raymond Christiansen