Buenas,
En este ejercicio se me ocurre escribir el tipo de addAB tal que el tipo resultado sea de la forma ABNat (1+(2^n)), en donde (1+(2^n)) expresa la cantidad de elementos para un arbol de altura n+1.
Ejemplo arbol de altura 2: ABNat (1+2^1) := ABNat (3).
La consulta es, estoy por el camino correcto? y en caso de que si, como se expresa la potencia en coq? de la forma que lo escribi aca obtengo el siguiente resultado Unknown interpretation for notation "_ ^ _".
Gracias
Saludos
Hola.
No es necesaria la operación de potencia. La idea es que en cada aplicación de addAB se permita construir un AB de altura n+1 a partir de dos subárboles de altura n. Restringiendo la altura de cada subárbol se logra que los árboles sean completos.
Siguiendo los ejemplos de la letra del práctico, cada árbol se podría generar del anterior con una aplicación de addAB, particiendo inicialmente (primer dibujo) de dos subárboles vacíos (de altura 0).
Si no queda clara la explicación, volvé a escribir.
Saludos, Carlos