3
User
Recs.
Recs.
6
Updates
Last
Updated
Updated
Activity
13 Options
Specs
Specs are quantitative aspects of the option such as the price
Pros
Pro Metaprogramming occurs in the same language as the theorem proving.
Because the metaprogramming occurs in the same level as the programming, you are able to write automated tactics that depend on mathematical objects you have already defined, and use those tactics to define more objects. It is a very powerful leap forward in automated and interactive theorem proving.
Know any positive aspects of this option?
Cons
Know any negative aspects of this option?