git.iko.soy/Idris-dev
on 4e69658 help sign in
history ofsrc/Idris/Reflection.hs
all commits
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 3592edbReflection for SN, plus an SN for meta-stuffDavid Raymond Christiansen 3047ae8Small formatting fixDavid Raymond Christiansen c51241fReflected elab: look up datatypesDavid Raymond Christiansen d97715ePlumb datatype information through the proof stateDavid Raymond Christiansen 04b4cc0Merge remote-tracking branch 'refs/remotes/upstream/master' into wip/tacticalDavid Raymond Christiansen 370939bMerge branch 'master' of github.com:idris-lang/Idris-devEdwin Brady e32e899Totality checking for functions defined in Elab scriptsDavid Raymond Christiansen 367c037Move quoters and unquoters to Idris.ReflectionDavid Raymond Christiansen 7d02904Progress towards defining functions in TacticalDavid Raymond Christiansen cfd6dbcStart of defining functions in TacticalDavid Raymond Christiansen 6d188c4Begin to use a sum type for post-elab IState tweaksDavid Raymond Christiansen c2dc6ecAllow new-style tactics to declare function signaturesDavid Raymond Christiansen