Una duda,
Se puede usar el tipo ArrayNat para definir AVLaddi?
Saludos,
Joaquín
Hola Joaquín.
Se podría usar pero no es necesario en este caso. Notar que el parámetro numérico refiere a la altura.
Un posibles AddAVLi (para el caso de árboles de naturales) sería por ejemplo:
Parameter addAVL1 : forall n, AVLNat n -> nat -> AVLNat n -> AVLNat (n + 1).
Notar que no es la única posibilidad de generar un AVL no vacío, ya que los subárboles podrían diferir respecto a sus alturas hasta en una unidad.
Saludos, Carlos
Entonces el rango de i no depende de la.altura del árbol?
No. El i es porque hay varios addAVL. Diría tres; dos adicionales al que mostré.
Saludos Carlos