search

marcusrossel / lean-egg

A (WIP) equality saturation tactic for Lean based on egg.
Apache License 2.0
41 stars 2 forks source link

Use `LeanApplier` for all Rewrites? #34

Open marcusrossel opened 1 month ago

marcusrossel commented 1 month ago

Right now we use the LeanApplier only for rewrites coming from Lean, but not those hardcoded by us in Rust. This might cause problems because that means that we don't get capture avoidance, etc. for those rewrites.

marcusrossel commented 1 month ago

We'd have to take care not to disable rewrites on primitive constructors in that case.