Commit cdf9fa69 authored by charguer's avatar charguer

added_lia

parent e0e42144
frederic.besson@inria.fr:
git clone https://gforge.inria.fr/git/ppsimpl/micromega.git
c’est un plugin micromega pour 8.5
Require Import Micromega.Lia
Il y a 2 options
Unset Lia Enum.
Pas de preuve par énumération.
Le prouveur devient incomplet sur Z — il raisonne comme si il était sur R.
Ça suffit pour ton but et je pense dans la plupart des cas.
Set Lia Depth n.
Qui limite la taille des preuve intermédaires.
Ton but passe avec profondeur 6…
Et ça échoue presque instantanément…
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment