**Problem:** We need to support writing recursive function directly, beside using recursive combinators. **Solution 1:** Implement Coq like `fixpoint`, `readback` should handle `fixpoint` to avoid infinite loop.
Problem:
We need to support writing recursive function directly, beside using recursive combinators.
Solution 1:
Implement Coq like
fixpoint,readbackshould handlefixpointto avoid infinite loop.