leanprover-community / mathlib

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

Zulip Chat Archive

Stream: general

Topic: todo axiom


Bernd Losert (Nov 29 2021 at 19:40):

Is there like a todo axiom that I can use in places where I don't know the definition/proof?

Kyle Miller (Nov 29 2021 at 19:42):

sorry

Kyle Miller (Nov 29 2021 at 19:43):

In a proof you can use the tactics sorry or admit (they're synonyms)

Bernd Losert (Nov 29 2021 at 19:43):

Sweet. Thanks.


Last updated: May 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll