On Dec 12, 2014, at 3:30 AM, Adam Gundry a...@well-typed.com wrote:
I did vaguely wonder about doing something like this, but was worried
about the complexity. Since you all seem keen, though, I'll have a go
and see if I can make it work. I'd imagine using the (plugin module
name, axiom
I've been following the plugins stuff at a small distance. I'vm very interested
as a user, but don't have the bandwidth to think deeply as an implementor. With
that caveat, I have a proposal:
Suppose plugin P is responsible for producing CoAxiomRule R while compiling
module M. I think it's
Go ahead and make suggestions here. Since a CoAxiomRule embodies essentially
arbitrary computation, it's hardly surprising that there's a fixed range of
possibilities.
I suppose that for extensibilty, any particular plugin could say
TypeNats:Rule1, TypeNats:Rule etc, and recognise that at the
Hello,
the reason there's a function there is that the type-nats are using an
infinite family of axioms (e..g, the axiom `AddDef` which can be applied to
any two concrete number, so `AddDef 1 2 : (1 + 2) ~ 3`).
Do you think it'd be possible to allow plugins to register a list of
axioms, so that
