The Coq mailing list

[roux cody <cody.roux AT gmail.com>]

I hope someone with more expertise will weigh in here, since I am a bit out of my depth. Still I'll try to answer some of the questions with the caveat that I'm not really an expert.

On 02/25/2016 10:29 AM, roux cody wrote:
> (though the Agda-style unicode bindings are just so fun!).
What do you mean?

I just mean I like the agda-style input which replaces \forall by the unicode ∀ seamlessly. It's possible that this is supported in coq as well I guess (I'm a little behind the times).

> Is there anything in lean-mode that is not described in https://leanprover.github.io/presentations/20150123_lean-mode/lean-mode.pdf ?

You'd really have to ask Soonho directly.

> Is there a way in Lean for users to define new tactics, as with Ltac?

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.

> 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