Investigate whether using `context` tactic to express proof mode tactics makes them more efficient (compared to computation) - Githubissues

harp-project / AML-Formalization

GNU Lesser General Public License v2.1

10 stars 5 forks source link

Investigate whether using `context` tactic to express proof mode tactics makes them more efficient (compared to computation) #427

Open berpeti opened 7 months ago

berpeti commented 7 months ago

This issue came up when defining mlConj with mlAssert