- Stanford University Centaur Lab
- https://leni.sh
-
Director of NorCal Hakkero Factory No. 1
- Joined on
2023-08-21
feat: Elementarized tactics with motives, congruence, and absurdity
I think the metavariables generated by mapply
don't have to be syntheticOpaque
, since no isDefEq
operation is contained in it, but we'll see if this is a problem.
Enable direct expression evaluation in context