• Andrei Paskevich's avatar
    add inline_goal to transform/inlining · 349a0eb4
    Andrei Paskevich authored
    + change inline_trivial: now we only inline right-linear
    definitions where no variable occurs deeper than level 1.
    Attention: this inlines definitions with arbitrarily complex
    ground terms on the right-hand side - which might be a BAD IDEA,
    but I still want to give it a try.
    + add find_logic_definition to Decl
inlining.mli 3.32 KB