FINITE MAGMA EXPLORER: Use the finite magma graph rather than the general magma graph to detect new refutations

teorth / equational_theories

A project to map out the relations between different equational theories of Magmas.

https://teorth.github.io/equational_theories/

Apache License 2.0

216 stars 51 forks source link

FINITE MAGMA EXPLORER: Use the finite magma graph rather than the general magma graph to detect new refutations #855

Closed teorth closed 26 minutes ago

teorth commented 3 hours ago

Pointed out in https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/Austin.20pairs/near/483160464

vlad902 commented 2 hours ago

I think this may be as easy as using --finite-only with lake exe extract_implications unknowns in the CI workflow, but I'm not very familiar with FME so someone should double check me.

vlad902 commented 2 hours ago

Actually, took a quick look, that seems right.

vlad902 commented 2 hours ago

claim

vlad902 commented 2 hours ago

propose PR #856