1. Implement exponent operation in front-end.
2. -loop options
3. Fix the front-end set target location for while loop.
4. convert the compare of two arrays into forall expressions in theorem prover
5. add \D in front-end
6. report syntax error more elegantly and clearly.
7. correct forall grammar.
8. 