Consultas de Práctico

Hola.

Hay cosas que cambiaron en la última versión de Coq.

1) Para que funcione Extraction Language Haskell, hay que poner primero algo:

Require Import Coq.extraction.ExtrHaskellBasic.

Extraction Language Haskell.

Extraction "predecesor" predspec.

2) Para usar functional induction en el ejercicio de mirror:

Require Import FunInd.

Functional Scheme inverse_ind := Induction for inverse Sort Prop.

Lemma MirrorC2 : forall (A : Set) (t : bintree A), {t2 : bintree A | mirror A t t2}.

Proof.

intros A t.

exists (inverse A t).

functional induction inverse A t.

...

Saludos, Carlos