{"size": 829, "ext": "scrbl", "max_stars_repo_path": "examples/euclid_gcd.scrbl", "max_stars_repo_name": "khinsen/leibniz-examples", "max_stars_repo_stars_event_min_datetime": "2017-03-22T08:37:51.000Z", "max_stars_repo_stars_event_max_datetime": "2020-10-12T22:58:00.000Z", "max_issues_repo_path": "examples/euclid_gcd.scrbl", "max_issues_repo_name": "khinsen/leibniz-examples", "max_issues_repo_issues_event_min_datetime": null, "max_issues_repo_issues_event_max_datetime": null, "max_forks_repo_path": "examples/euclid_gcd.scrbl", "max_forks_repo_name": "khinsen/leibniz-examples", "max_forks_repo_forks_event_min_datetime": "2018-02-05T07:35:03.000Z", "max_forks_repo_forks_event_max_datetime": "2020-10-12T22:58:02.000Z"}
{"max_stars_count": 2, "max_issues_count": null, "max_forks_count": 3, "avg_line_length": 31.8846153846, "max_line_length": 146, "alphanum_fraction": 0.599517491}
#lang leibniz

@title{The greatest common divisor of two natural numbers}
@author{Euclid}

@context["gcd" #:use "builtins/integers"]{

The greatest common divisor @op{gcd(a:ℕ, b:ℕ) : ℕ} of two natural numbers @var{a:ℕ} and @var{b:ℕ} can be obtained by applying the following rules:
@itemlist[#:style 'ordered
  @item{If the two numbers are equal, their GCD is equal to them as well:
            @linebreak[]
            @rule{gcd(a, a) ⇒ a}}
  @item{If a > b, replace a by a-b:
            @linebreak[]
            @rule{gcd(a, b) ⇒ gcd(a - b, b) if a > b}}
  @item{Otherwise we have b > a and replace b by b-a:
            @linebreak[]
            @rule{gcd(a, b) ⇒ gcd(a, b - a)}}]

Here are some application examples:
@itemlist[
  @item{@eval-term{gcd(2, 3)}}
  @item{@eval-term{gcd(3, 2)}}
  @item{@eval-term{gcd(42, 7)}}]

}