ufmg-smite / lean-smt

Tactics for discharging Lean goals into SMT solvers.
Apache License 2.0
89 stars 18 forks source link

Use attribute to mark transformers. #10

Closed abdoo8080 closed 2 years ago

abdoo8080 commented 2 years ago

This PR breaks down Smt.Transformer module into multiple ones (one for each theory). It introduces a new Lean attribute, [smt], to track markers/transformers in those modules and retrieve them at run-time. More attributes will be added in the feature to modularize the system. This is also work towards refactoring Smt.Transformer.