Skip to content

Instantly share code, notes, and snippets.

@gallais
Created Dec 17, 2019
Embed
What would you like to do?
example of search
open import Agda.Builtin.Equality
open import Agda.Builtin.Nat hiding (_+_; _<_)
open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary
-- C-c C-z RET _*_ _≡_ RET
-- returns
-- Definitions about _*_, _≡_
-- *-cancelʳ-≡
-- : (m n : ℕ) {o : ℕ} → m * suc o ≡ n * suc o → m ≡ n
-- *-cancelˡ-≡
-- : {m n : ℕ} (o : ℕ) → m + o * m ≡ n + o * n → m ≡ n
-- *-suc : (m n : ℕ) → m * suc n ≡ m + m * n
-- +-*-suc : (m n : ℕ) → m * suc n ≡ m + m * n
-- ^-*-assoc : (m n o : ℕ) → ((m ^ n) ^ o) ≡ (m ^ (n * o))
-- ^-distribˡ-+-*
-- : (m n o : ℕ) → (m ^ (n + o)) ≡ (m ^ n) * (m ^ o)
-- cancel-*-right
-- : (m n : ℕ) {o : ℕ} → m * suc o ≡ n * suc o → m ≡ n
-- i*j≡0⇒i≡0∨j≡0
-- : (m : ℕ) {n : ℕ} → m * n ≡ 0 → m ≡ 0 Data.Sum.Base.⊎ n ≡ 0
-- i*j≡1⇒i≡1 : (m n : ℕ) → m * n ≡ 1 → m ≡ 1
-- i*j≡1⇒j≡1 : (m n : ℕ) → m * n ≡ 1 → n ≡ 1
-- im≡jm+n⇒[i∸j]m≡n
-- : (i j m n : ℕ) → i * m ≡ j * m + n → (i ∸ j) * m ≡ n
-- m*n≡0⇒m≡0∨n≡0
-- : (m : ℕ) {n : ℕ} → m * n ≡ 0 → m ≡ 0 Data.Sum.Base.⊎ n ≡ 0
-- m*n≡1⇒m≡1 : (m n : ℕ) → m * n ≡ 1 → m ≡ 1
-- m*n≡1⇒n≡1 : (m n : ℕ) → m * n ≡ 1 → n ≡ 1
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment