I don't know why you say that, but I'd be willing to be convinced. The main source of great automation in Isabelle is the ability to rewrite by thousands of equalities, and therefore the very flexible notion of equality in Isabelle that supports e.g. quotients
Conversation
You get the same exact thing out of path equality in cubical, but nobody who likes cubical cares about automation
2
1
Cubical + e-graphs boom you're done
4
1
Can e-graphs be done fast? I looked at them a bit but it seemed they were taking a pretty slow approach to name binding/substitution. Would be cool to figure out how to get e-graphs to work with the semantic type checking stuff - is that possible at all?
2
2
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
It is, but we have the work in Lean to build off of, except our job is easier since our notion of equality & congruence is nicer
1
1
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
Yeah, that's the work I thought was being talked about - I was looking at the implementation and trying to understand it, but was a bit discouraged by the approach to substitution. Was hoping there might be a way to get around this… :(
1
Was talking to Chase Wilson about this today, and it seems that it's not necessary to use the `define_language!` thing in the egg crate! You just need to implement stuff manually. And then the `Analysis` trait can be impled where`Self::Data = Value`: docs.rs/egg/0.6.0/egg/
1
So it seems like it _might_ be possible to integrate it into a semantic type checker – I haven't tried it yet though, but it could be fun to have a go at some stage!
Woops, forgot to de-@ Liam and Sam, was just intending to reply to Jon and Talia about this! 😳