forked from GitHub/gf-core
62 lines
1.9 KiB
HTML
62 lines
1.9 KiB
HTML
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
|
|
<HTML>
|
|
<HEAD>
|
|
<META NAME="generator" CONTENT="http://txt2tags.sf.net">
|
|
</HEAD><BODY BGCOLOR="white" TEXT="black">
|
|
<FONT SIZE="4">
|
|
</FONT></CENTER>
|
|
|
|
<P></P>
|
|
<HR NOSHADE SIZE=1>
|
|
<P></P>
|
|
<P></P>
|
|
<HR NOSHADE SIZE=1>
|
|
<P></P>
|
|
<P>
|
|
Last update: Tue Jan 10 21:50:58 2006
|
|
</P>
|
|
<P>
|
|
Produced by
|
|
gfdoc - a rudimentary GF document generator.
|
|
(c) Aarne Ranta (<A HREF="mailto:aarne@cs.chalmers.se">aarne@cs.chalmers.se</A>) 2002 under GNU GPL.
|
|
</P>
|
|
<P>
|
|
numerals from 1 to 999999 in decimal notation
|
|
</P>
|
|
<PRE>
|
|
abstract Numeral = Cat ** {
|
|
|
|
cat
|
|
Digit ; -- 2..9
|
|
Sub10 ; -- 1..9
|
|
Sub100 ; -- 1..99
|
|
Sub1000 ; -- 1..999
|
|
Sub1000000 ; -- 1..999999
|
|
|
|
fun
|
|
num : Sub1000000 -> Numeral ;
|
|
|
|
n2, n3, n4, n5, n6, n7, n8, n9 : Digit ;
|
|
|
|
pot01 : Sub10 ; -- 1
|
|
pot0 : Digit -> Sub10 ; -- d * 1
|
|
pot110 : Sub100 ; -- 10
|
|
pot111 : Sub100 ; -- 11
|
|
pot1to19 : Digit -> Sub100 ; -- 10 + d
|
|
pot0as1 : Sub10 -> Sub100 ; -- coercion of 1..9
|
|
pot1 : Digit -> Sub100 ; -- d * 10
|
|
pot1plus : Digit -> Sub10 -> Sub100 ; -- d * 10 + n
|
|
pot1as2 : Sub100 -> Sub1000 ; -- coercion of 1..99
|
|
pot2 : Sub10 -> Sub1000 ; -- m * 100
|
|
pot2plus : Sub10 -> Sub100 -> Sub1000 ; -- m * 100 + n
|
|
pot2as3 : Sub1000 -> Sub1000000 ; -- coercion of 1..999
|
|
pot3 : Sub1000 -> Sub1000000 ; -- m * 1000
|
|
pot3plus : Sub1000 -> Sub1000 -> Sub1000000 ; -- m * 1000 + n
|
|
}
|
|
</PRE>
|
|
<P></P>
|
|
|
|
<!-- html code generated by txt2tags 2.3 (http://txt2tags.sf.net) -->
|
|
<!-- cmdline: txt2tags -thtml -\-toc abstract/Numeral.txt -->
|
|
</BODY></HTML>
|