Real-time collaboration for Jupyter Notebooks, Linux Terminals, LaTeX, VS Code, R IDE, and more,
all in one place.
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: 18536License: APACHE
import tactic.localized
open tactic
local infix ` ⊹ `:59 := nat.mul
local infix ` ↓ `:59 := nat.pow
local infix ` ⊖ `:59 := nat.pow
example : 2 ⊹ 3 = 6 := rfl
example : 2 ↓ 3 = 8 := rfl
example : 2 ⊖ 3 = 8 := rfl
example {n m : ℕ} (h : n < m) : n ≤ m := by { success_if_fail { simp [h] }, exact le_of_lt h }
section
localized "infix ` ⊹ `:59 := nat.add" in nat
localized "infix ` ↓ `:59 := nat.mul" in nat
localized "infix ` ⊖ `:59 := nat.mul" in nat.mul
localized "attribute [simp] le_of_lt" in le
example : 2 ⊹ 3 = 5 := rfl
example : 2 ↓ 3 = 6 := rfl
example : 2 ⊖ 3 = 6 := rfl
example {n m : ℕ} (h : n < m) : n ≤ m := by { simp [h] }
end
section
example : 2 ⊹ 3 = 6 := rfl
example : 2 ↓ 3 = 8 := rfl
example : 2 ⊖ 3 = 8 := rfl
example {n m : ℕ} (h : n < m) : n ≤ m := by { success_if_fail { simp [h] }, exact le_of_lt h }
open_locale int
example : 2 ⊹ 3 = 6 := rfl
example : 2 ↓ 3 = 8 := rfl
example : 2 ⊖ 3 = 8 := rfl
open_locale nat
example : 2 ⊹ 3 = 5 := rfl
example : 2 ↓ 3 = 6 := rfl
example : 2 ⊖ 3 = 8 := rfl
open_locale nat.mul
example : 2 ⊹ 3 = 5 := rfl
example : 2 ↓ 3 = 6 := rfl
example : 2 ⊖ 3 = 6 := rfl
end
section
open_locale nat.mul nat nat.mul int le
example : 2 ⊹ 3 = 5 := rfl
example : 2 ↓ 3 = 6 := rfl
example : 2 ⊖ 3 = 6 := rfl
example {n m : ℕ} (h : n < m) : n ≤ m := by { simp [h] }
end