Commit a0c12333 authored by Frontull Samuel's avatar Frontull Samuel
Browse files

fixed weak_step application case

parent f5d7933c
......@@ -173,8 +173,8 @@ let rec _weak_step term pos p =
| LApp (LLam (l, v, b), arg) ->
if p = pos then beta term
else if starts_with (p ^ "1") pos then
_weak_step (LLam (l, v, b)) pos (p ^ "1")
else _weak_step arg pos (p ^ "2")
LApp (_weak_step (LLam (l, v, b)) pos (p ^ "1"), arg)
else LApp (LLam (l, v, b), _weak_step arg pos (p ^ "2"))
| LApp (e1, e2) ->
LApp (_weak_step e1 pos (p ^ "1"), _weak_step e2 pos (p ^ "2"))
| LLam (l, x, e) -> LLam (l, x, _weak_step e pos (p ^ "1"))
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment