Local hints need to reduce (just like global hints do) so we expand
their definition to the lifted name before applying them.
We're identifying the global hints by knowing that the binder name is a
nested function name. This is a bit of hack, and it'd probably be better
to record that information in the binder instead, but that's a more
substantial change than I want to do right now.
This gives us the ability to define and use implementations locally, in
where clauses/local let bindings, as well as flag local definitions as
hints.
It's not yet quite equivalent to global hints, however, since it translated
the hint to a local let binding, which doesn't reduce, so if something
relies on the reduction behaviour of the hint, it won't work. This
refinement is coming later
+ Expanded the documentation on how to use literate modes.
+ Added invisible code blocks in Markdown using specially tagged comment blocks: `<!-- idris -->`.
+ Fixed OrgMode specificaton to recognise comment blocks properly.
This involves a small extension to IPragma, because to properly
elaborate names in a local scope we need to know which names are defined
in that scope so that they get applied to the environment when needed.
This means we can now define implementations of interfaces locally (but
there's still some work to do, because we don't yet have a way of
applying locally defined hints in auto search. It's coming soon!)
This allows, for exmaple, to have apostrophes in module names.
Test was added only for chez, however this should be viable for all
targets with `:exec` implemented.
module, then the current namespace (accessed by calling getNS) differs
from the function namespace, therefore it is not considered visible by
TTImp.Elab.App.checkVisibleNS
Gambit after version v4.9.3 supports the -cc option, which configures
the compiler backend Gambit will use to build the binary. Currently to
get this functionality Gambit needs to be built from source, since it is
not yet available in a released version.
