Skip to main content

Browse the archive

Revision 503d035509bd518c18a45b04244b317c75204d7e authored by Pierre Boutry on 19 March 2024, 10:29:37 UTC, committed by Pierre-Yves Strub on 05 April 2024, 18:16:56 UTC 
Polynomial division
1 parent 30bfa95
Raw File
fail.ec 
(* -------------------------------------------------------------------- *)
require import AllCore.

(* -------------------------------------------------------------------- *)
lemma L (p q : bool) : p => q.
proof.
move=> h.
fail apply: h.
abort.
back to top