Introducción
El grupo de kínder está aprendiendo sobre el cultivo de plantas.
A la maestra le pareció buena idea darle a la clase semillas para sembrar y cultivar en la tierra.
Con ese fin, los niños colocaron vasitos a lo largo de las repisas de las ventanas y sembraron un tipo de planta en cada vasito.
Los niños pudieron elegir sus favoritas entre cuatro tipos de semillas disponibles: grass, clover, radishes y violets.
Instrucciones
Tu tarea es, a partir de un diagrama, determinar qué plantas le corresponden a cada estudiante de la clase del kínder.
En la clase hay 12 estudiantes:
- Alice, Bob, Charlie, David, Eve, Fred, Ginny, Harriet, Ileana, Joseph, Kincaid y Larry.
Se plantan cuatro tipos distintos de semillas:
| Planta |
Codificación en el diagrama |
| Grass |
G |
| Clover |
C |
| Radish |
R |
| Violet |
V |
Cada estudiante recibe cuatro vasos, dos en cada fila:
[window][window][window]
........................ # each dot represents a cup
........................
Su docente asigna los vasos a los estudiantes en orden alfabético según sus nombres, así que Alice va primero y Larry va al final.
Este es un diagrama de ejemplo que representa las plantas de Alice:
[window][window][window]
VR......................
RG......................
En la primera fila, la más cercana a las ventanas, tiene una violet y un radish.
En la segunda fila tiene un radish y un poco de grass.
A tu programa se le darán las plantas de izquierda a derecha, empezando por la fila más cercana a las ventanas.
Con esto, debe poder determinar qué plantas le pertenecen a cada estudiante.
Por ejemplo, si se le dice que el jardín se ve así:
[window][window][window]
VRCGVVRVCGGCCGVRGCVCGCGV
VRCCCGCRRGVCGCRVVCVGCGCV
Entonces, si se le piden las plantas de Alice, debe devolver:
- Violets, radishes, violets, radishes
Y si se le piden las plantas de Bob, daría:
- Clover, grass, clover, clover
Vectores
El valor de retorno de la función plants es un Vector Plant 4.
Los vectores representan arrays de longitud fija.
Esta longitud también puede determinarse en tiempo de ejecución.
Se pueden pensar como un par que consiste en un Array y una prueba de que el array tiene la longitud requerida.
Esto significa que debes proporcionar esta prueba para poder construir un Vector.
Este capítulo ofrece una buena introducción a la demostración de teoremas en Lean.
Para profundizar más, este libro figura como recurso oficial en el sitio web de Lean.
Lean ofrece muchas tácticas que pueden automatizar una prueba o partes de ella.
Quizás quieras consultar una referencia del lenguaje.
