مقدمة
يتعلّم صف رياض الأطفال زراعة النباتات. ورأت المعلّمة أن من الجيد أن تمنح الصف بذورًا ليزرعوها وينمّوها في التراب. وتحقيقًا لذلك، وضع الأطفال أكوابًا صغيرة على طول عتبات النوافذ، وزرعوا في كل كوب نوعًا واحدًا من النبات. وقد أتيح للأطفال أن يختاروا ما يفضلونه من بين أربعة أنواع متاحة من البذور: grass وclover وradishes وviolets.
التعليمات
مهمتك هي أن تحدد، انطلاقًا من مخطط، النباتات المسؤول عنها كل طفل في صف رياض الأطفال.
يوجد في الصف 12 طفلًا:
- Alice وBob وCharlie وDavid وEve وFred وGinny وHarriet وIleana وJoseph وKincaid وLarry.
تُزرع أربعة أنواع مختلفة من البذور:
| النبات |
ترميز المخطط |
| Grass |
G |
| Clover |
C |
| Radish |
R |
| Violet |
V |
يحصل كل طفل على أربعة أكواب، اثنان في كل صف:
[window][window][window]
........................ # each dot represents a cup
........................
يخصّص المعلّم الأكواب للأطفال وفق الترتيب الأبجدي لأسمائهم، وهذا يعني أن Alice تأتي أولًا وLarry يأتي أخيرًا.
وهذا مثال على مخطط يمثّل نباتات Alice:
[window][window][window]
VR......................
RG......................
في الصف الأول، الأقرب إلى النوافذ، لديها Violet وRadish.
وفي الصف الثاني لديها Radish وGrass.
سيتلقّى برنامجك النباتات من اليسار إلى اليمين، بدءًا من الصف الأقرب إلى النوافذ.
ومن هذا، ينبغي أن يقدر على تحديد النباتات التي تنتمي إلى كل طالب.
على سبيل المثال، إذا قيل له إن الحديقة تبدو هكذا:
[window][window][window]
VRCGVVRVCGGCCGVRGCVCGCGV
VRCCCGCRRGVCGCRVVCVGCGCV
فإذا سُئل عن نباتات Alice، فعليه أن يعطي:
- Violets, radishes, violets, radishes
أما إذا سُئل عن نباتات Bob، فسينتج:
- Clover, grass, clover, clover
المتجهات
القيمة التي تُرجعها دالة plants هي Vector Plant 4.
تمثل المتجهات مصفوفات ذات طول ثابت.
ويمكن أيضًا تحديد هذا الطول في وقت التشغيل.
ويمكن التفكير فيها كزوج يتكون من Array وبرهان على أن المصفوفة تملك الطول المطلوب.
هذا يعني أنه يجب عليك تقديم هذا البرهان لبناء Vector.
يقدّم هذا الفصل مقدمة جيدة لإثبات النظريات في Lean.
ولمزيد من التعمق، يُدرج هذا الكتاب كمصدر رسمي على موقع Lean.
تقدم Lean العديد من التكتيكات التي يمكنها أتمتة برهان أو أجزاء منه.
قد ترغب في الاطلاع على مرجع اللغة.
