mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(Mathlib/Tactic/TypeCheck): add `type_check` tactic

Open j-loreaux opened this issue 3 years ago • 1 comments

Lean 3 version: https://github.com/leanprover-community/lean/blob/master/library/init/meta/interactive.lean#L1664

j-loreaux avatar Jul 18 '22 21:07 j-loreaux

Gotta add it to the Mathlib.lean import list 👍🏼

arthurpaulino avatar Jul 18 '22 23:07 arthurpaulino

Thank!

bors r+

gebner avatar Sep 08 '22 17:09 gebner

Pull request successfully merged into master.

Build succeeded:

bors[bot] avatar Sep 08 '22 17:09 bors[bot]