mirror of
https://github.com/GrammaticalFramework/gf-rgl.git
synced 2026-06-30 02:58:35 -06:00
(Hun) Remove unnecessary distinction between digits and numbers
This commit is contained in:
@@ -112,7 +112,7 @@ param
|
||||
|
||||
CardOrd = NOrd | NCard ; -- Not used yet
|
||||
|
||||
NumType = NoNum | IsDig | IsNum ;
|
||||
NumType = NoNum | IsNum ;
|
||||
|
||||
oper
|
||||
isNum : {numtype : NumType} -> Bool = \nt -> case nt.numtype of {
|
||||
|
||||
Reference in New Issue
Block a user