forked from GitHub/gf-rgl
(Kor) Add Digits
This commit is contained in:
@@ -96,7 +96,11 @@ concrete NounKor of Noun = CatKor ** open ResKor, Prelude in {
|
||||
NumCard card = card ;
|
||||
|
||||
-- : Digits -> Card ;
|
||||
-- NumDigits dig =
|
||||
NumDigits dig = baseNum ** {
|
||||
s = \\_,_ => dig.s ! NCard ;
|
||||
n = dig.n ;
|
||||
numtype = IsDig
|
||||
} ;
|
||||
|
||||
-- : Numeral -> Card ;
|
||||
NumNumeral num = num ;
|
||||
|
||||
@@ -84,7 +84,6 @@ lin
|
||||
-- : Sub1000 -> Sub1000 -> Sub1000000 ; -- m * 1000 + n
|
||||
pot3plus m n = TODO ;
|
||||
|
||||
|
||||
oper
|
||||
LinDigit : Type = ResKor.Numeral ** {isTwo : Bool ; ten : Str} ;
|
||||
|
||||
@@ -123,4 +122,45 @@ oper
|
||||
} ;
|
||||
|
||||
TODO : ResKor.Numeral = mkNum2 "TODO" "TODO" ;
|
||||
|
||||
|
||||
-- numerals as sequences of digits
|
||||
|
||||
lincat
|
||||
Dig = TDigit ;
|
||||
|
||||
lin
|
||||
-- : Dig -> Digits ; -- 8
|
||||
IDig d = d ;
|
||||
|
||||
-- : Dig -> Digits -> Digits ; -- 876
|
||||
IIDig d i = {
|
||||
s = \\o => d.s ! NCard ++ BIND ++ i.s ! o ;
|
||||
n = Pl
|
||||
} ;
|
||||
|
||||
D_0 = mkDig "0" ;
|
||||
D_1 = mk3Dig "1" "1번째" ResKor.Sg ;
|
||||
D_2 = mkDig "2" ;
|
||||
D_3 = mkDig "3" ;
|
||||
D_4 = mkDig "4" ;
|
||||
D_5 = mkDig "5" ;
|
||||
D_6 = mkDig "6" ;
|
||||
D_7 = mkDig "7" ;
|
||||
D_8 = mkDig "8" ;
|
||||
D_9 = mkDig "9" ;
|
||||
|
||||
oper
|
||||
mk2Dig : Str -> Str -> TDigit = \c,o -> mk3Dig c o ResKor.Pl ;
|
||||
mkDig : Str -> TDigit = \c -> mk2Dig c (c + "번째") ;
|
||||
|
||||
mk3Dig : Str -> Str -> ResKor.Number -> TDigit = \c,o,n -> {
|
||||
s = table {NCard => c ; NOrd => o} ;
|
||||
n = n
|
||||
} ;
|
||||
|
||||
TDigit = {
|
||||
n : ResKor.Number ;
|
||||
s : CardOrd => Str
|
||||
} ;
|
||||
}
|
||||
|
||||
Reference in New Issue
Block a user