Le 06/07/2016 08:15, Julian 1 a écrit :
> Is this transformation different than using the 'inductive'
> builtin/keyword to create an inductive symbol/theory.

Yes!

- Claude

-- 
Claude Marché                          | tel: +33 1 69 15 66 08
INRIA Saclay - Île-de-France           |
Université Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex                    |
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
http://lists.gforge.inria.fr/mailman/listinfo/why3-club

Reply via email to