mathlib
3c3c3bc1 - fix(tactic/interactive): use non-interactive admit tactic (#12489)

Commit

4 years ago

fix(tactic/interactive): use non-interactive admit tactic (#12489) In a future release of Lean 3, the interactive admit tactic will take an additional argument.

Author

kmill

Parents

5f2a6ac6

mathlib 3c3c3bc1 - fix(tactic/interactive): use non-interactive admit tactic (#12489)

mathlib
3c3c3bc1 - fix(tactic/interactive): use non-interactive admit tactic (#12489)