The Coq mailing list

[Chris Casinghino <chris.casinghino AT gmail.com>]

Hi Adam,

Thanks for the quick response.  You're certainly right, and I should
have been a little clearer.  I'm interested specifically in logical
consistency, and am not concerned about extraction or the fact that
the axiom will get in the way of reduction.

--Chris

> Such an axiom certainly breaks extraction, since it has no natural
> computational interpretation, but perhaps you don't care about extraction.
> It also makes Gallina "computation" highly non-computational, which also
> might not bother you, depending on the application.  I don't know if it's
> logically consistent.