The Coq mailing list

[Dominic Mulligan <dominic.p.mulligan AT googlemail.com>]

Not really at the moment. This is a definite drawback (though Isabelle users don't seem so gung-ho about this). You can sort of pretend with the Lua bindings, I think.

The last couple of versions of Isabelle have an embedded proof method DSL called Eisbach, inspired by LTac:

http://ssrg.nicta.com.au/publications/nictaabstracts/7847.pdf

 

> Is there any extraction capability?

It's in the works.

> As for building-in proof irrelevance (while having a separate HoTT mode) that might not bother anyone but me: I (ab)use proof *relevance* in Coq as a way to get really good erasability.

I'm confused about this. Could you elaborate? Proof-irrelevance and proof erasure seem to go rather well together, in my mind.

> I wonder if runs into the same issues that Coq did. See "Meta-theory à la
> Carte", section "The Problem of Church Encodings and Induction",
> http://people.csail.mit.edu/bendy/MTC/.

Unless I misunderstand, the problem there seems to concern church encodings in pure CoC (as opposed to CIC), so not much to do with how inductives are implemented.

Best,

Cody

This email has been sent from a virus-free computer protected by Avast.
www.avast.com

On Thu, Feb 25, 2016 at 6:01 PM, Daniel Schepler <dschepler AT gmail.com> wrote:

On Thu, Feb 25, 2016 at 2:46 PM, Abhishek Anand
<abhishek.anand.iitg AT gmail.com> wrote:
> MathClasses has something similar, which I like a lot:
>
> http://www.cs.cornell.edu/~aa755/ROSCoq/coqdoc/MathClasses.misc.decision.html

OK, there's a lot of stuff otherwise in MathClasses that I wish would
make its way into the standard library, too.  I just hadn't noticed
that one - though it does seem like it could still use more extension
along the lines I was thinking.  (For example, I see and_dec and
or_dec there, but no impl_dec.)
--
Daniel Schepler