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
import
  tactic.alias
  tactic.cache
  tactic.clear
  tactic.converter.interactive
  tactic.core
  tactic.ext
  tactic.generalize_proofs
  tactic.interactive
  tactic.suggest
  tactic.lift
  tactic.localized
  tactic.mk_iff_of_inductive_prop
  tactic.push_neg
  tactic.rcases
  tactic.replacer
  tactic.restate_axiom
  tactic.rewrite
  tactic.lint
  tactic.simpa
  tactic.simps
  tactic.split_ifs
  tactic.squeeze
  tactic.well_founded_tactics
  tactic.where