Commit 50b75d2f authored by Andrei Paskevich's avatar Andrei Paskevich

add "eliminate_if" to why3_total_elimination.drv

parent d2ccb487
printer "why3"
filename "%f-%t-%g.why"
transformation "compile_match"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "compile_match"
transformation "eliminate_algebraic"
transformation "eliminate_if"
transformation "eliminate_let"
theory BuiltIn
......
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