The Coq mailing list

[Jacques-Henri Jourdan <jacques-henri.jourdan AT inria.fr>]

Well, using <: is the same thing as using vm_compute.

-- 
JH

Le 25/03/2015 17:29, Jonathan Leivent a écrit :
>
>
> On 03/25/2015 03:05 AM, Stefan Ciobaca wrote:
>> The development is here:
>>
>> https://github.com/clarus/falso
>>
>>  From the readme:
>>
>> "This is an implementation in the Coq proof assistant of the Falso proof
>> system. It exploits a bug of thevm_compute command when there is a type
>> with more than 255 constructors. The vm_computecommand evaluates a term
>> efficiently by compilation to a byte-code. This bug concerns all recent
>> versions of Coq, including Coq 8.4pl5."
>>
>> Cheers,
>> Stefan Ciobaca
>>
>
> I don't think it is limited to vm_compute.  For instance, I was able
> to do this without vm_compute:
>
> Lemma inconsistency : true = false.
>   pose ((@eq_refl bool false<:@eq bool (is_256 (C_256 O)) false)
>           :@eq bool (is_256 (C_256 O)) false).
>   assumption.
> Qed.
>
> This is using 8.5beta.
>
> -- Jonathan
>

Attachment: signature.asc
Description: OpenPGP digital signature