<commit_before>------------------------------------------------------------------------------
-- The relation of divisibility on partial natural numbers
------------------------------------------------------------------------------

module FOTC.Data.Nat.Divisibility.By0 where

open import FOTC.Base

open import FOTC.Data.Nat

-- We add 3 to the fixities of the standard library.
infix 7 _∣_

------------------------------------------------------------------------------
-- The relation of divisibility.
-- The symbol is '\mid' not '|'.
-- It seems there is not agreement about if 0∣0, e.g.
-- * Agda standard library, version 0.5: 0|0
-- * Coq 8.3pl2: 0∣0
-- * Hardy and Wright. An introduction to the theory of numbers. 1975. 4ed: 0∤0
-- * Isabelle, version Isabelle2011: 0∣0
--
-- In our definition 0∣0, which is used to prove properties of the gcd as
-- it is in GHC HEAD (7.1.20110615), where gcd 0 0 = 0 (see
-- http://hackage.haskell.org/trac/ghc/ticket/3304).
_∣_ : D → D → Set
d ∣ e = ∃ λ k → N k ∧ e ≡ k * d
{-# ATP definition _∣_ #-}<commit_msg>Updated doc.<commit_after>------------------------------------------------------------------------------
-- The relation of divisibility on partial natural numbers
------------------------------------------------------------------------------

module FOTC.Data.Nat.Divisibility.By0 where

open import FOTC.Base

open import FOTC.Data.Nat

-- We add 3 to the fixities of the standard library.
infix 7 _∣_

------------------------------------------------------------------------------
-- The relation of divisibility.
-- The symbol is '\mid' not '|'.
-- It seems there is not agreement about if 0∣0, e.g.
-- * Agda standard library, version 0.5: 0|0
-- * Coq 8.3pl2: 0∣0
-- * Hardy and Wright. An introduction to the theory of numbers. 1975. 4ed: 0∤0
-- * Isabelle, version Isabelle2011: 0∣0
--
-- In our definition 0∣0, which is used to prove properties of the gcd
-- as it is in GHC 7.2.1, where gcd 0 0 = 0 (see
-- http://hackage.haskell.org/trac/ghc/ticket/3304).
_∣_ : D → D → Set
d ∣ e = ∃ λ k → N k ∧ e ≡ k * d
{-# ATP definition _∣_ #-}
{'fraction_non_alphanumeric': 0.32413136601618275, 'fraction_numerical': 0.0404569252736792, 'mean_word_length': 1.3459821428571428, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6946399', 'n_tokens_mistral': 717, 'n_tokens_neox': 616, 'n_words': 252}