Vs rule params (WIP) - Githubissues

mattulbrich / dive

Dafny Interactive Verification Environment (DIVE)

GNU General Public License v3.0

4 stars 0 forks source link

Vs rule params (WIP) #207

Open SpringVaS opened 2 years ago

SpringVaS commented 2 years ago

Recategorized QuantifierInstantiationRule as FocusProofRule, so it is now suggestedm if applicable.

Quick fix for #206. Discuss heap representation. Currently they are of type ApplTerm. Should ApplTerms generally be handled differently in substitutions? When do complications arise?