lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard

simp_procs for `simp`

Open leodemoura opened this issue 3 years ago • 0 comments
trafficstars

@digama0 and I want to make sure tactics such as Ring can be invoked from simp.

leodemoura avatar Jul 21 '22 21:07 leodemoura