File: Mgcd.mod

package info (click to toggle)
cafeobj 1.6.0-2
  • links: PTS, VCS
  • area: main
  • in suites: bookworm, bullseye, sid
  • size: 19,900 kB
  • sloc: lisp: 85,055; sh: 659; makefile: 437; perl: 147
file content (21 lines) | stat: -rw-r--r-- 451 bytes parent folder | download | duplicates (4) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
 
require Msimple-nat+

module GCD {
  protecting (SIMPLE-NAT+)
  op gcd : Nat Nat -> Nat
  -- --------------------
  vars N M : Nat
  ceq gcd(N, M) = gcd(M, N) if N < M .
  eq gcd(N, 0) = N .
  ceq gcd(s(N), s(M)) = gcd(s(N) - s(M), s(M))
  if not (N < M) .
}

provide Mgcd
--
eof
-- ==============================================
select GCD
reduce gcd(s(s(s(s(s(s(0)))))), s(s(s(s(0))))) .

** $Id: Mgcd.mod,v 1.1.1.1 2003-06-19 08:30:11 sawada Exp $