leanprover-community / mathlib

  • Home
  • Zulip archive
  • API documentation
  • Lean web editor
  • Links

Zulip Chat Archive

Stream: general

Topic: why lean-repl can't identify "norm_num" tactic?


Zihao Zhang (Dec 19 2024 at 06:50):

Screenshot from 2024-12-19 14-26-16.png

Kim Morrison (Feb 01 2025 at 06:26):

@Zihao Zhang, is it just that you didn't specify the "env" field of your second command, so you're working in a fresh environment without the import Mathlib?


Last updated: May 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll