Commit f04a1df0 authored by Andrei Paskevich's avatar Andrei Paskevich

accept let-expressions in inductive predicates

parent e2e2720a
......@@ -520,6 +520,9 @@ let create_ind_decl s idl =
| Tquant (Tforall, f) ->
let _,_,f = t_open_quant f in clause acc f
| Tbinop (Timplies, g, f) -> clause (g::acc) f
| Tlet (t, bf) ->
let v, f = t_open_bound bf in
clause (t_equ (t_var v) t :: acc) f
| _ -> (acc, f)
in
let cls, g = clause [] (check_fvs f) in
......
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