CoCalc Logo Icon
StoreFeaturesDocsShareSupportNewsAboutSign UpSign In

Real-time collaboration for Jupyter Notebooks, Linux Terminals, LaTeX, VS Code, R IDE, and more,
all in one place.

| Download

Try doing some basic maths questions in the Lean Theorem Prover. Functions, real numbers, equivalence relations and groups. Click on README.md and then on "Open in CoCalc with one click".

Project: Xena
Views: 18536
License: APACHE
Tweet
Share
Share
/-
This file imports many useful tactics ("the kitchen sink").

You can use `import tactic` at the beginning of your file to get everything.
(Although you may want to strip things down when you're polishing.)

Because this file imports some complicated tactics, it has many transitive dependencies
(which of course may not use `import tactic`, and must import selectively).

As (non-exhaustive) examples, these includes things like:
* algebra.group_power
* algebra.ordered_ring
* data.rat
* data.nat.prime
* data.list.perm
* data.set.lattice
* data.equiv.encodable
* order.complete_lattice
-/
import
  tactic.basic
  tactic.monotonicity.interactive
  tactic.finish
  tactic.tauto
  tactic.tidy
  tactic.abel
  tactic.ring
  tactic.ring_exp
  tactic.linarith
  tactic.omega
  tactic.wlog
  tactic.tfae
  tactic.apply_fun
  tactic.apply
  tactic.suggest
  tactic.simp_rw