lean4
lean4 copied to clipboard
simp_procs for `simp`
trafficstars
@digama0 and I want to make sure tactics such as Ring can be invoked from simp.