forked from GitHub/gf-core
small adjustments in grs
This commit is contained in:
@@ -34,16 +34,18 @@ fun
|
||||
def
|
||||
one = succ zero ;
|
||||
two = succ one ;
|
||||
sum m zero = m ;
|
||||
sum m (succ n) = succ (sum m n) ;
|
||||
prod m zero = zero ;
|
||||
sum m zero = m ;
|
||||
prod m (succ n) = sum (prod m n) m ;
|
||||
prod m zero = zero ;
|
||||
LtNat m n = Exist Nat (\x -> EqNat n (sum m (succ x))) ;
|
||||
Div m n = Exist Nat (\x -> EqNat m (prod x n)) ;
|
||||
Prime n = Conj
|
||||
(LtNat one n)
|
||||
(Univ Nat (\x -> Impl (Conj (LtNat one x) (Div n x)) (EqNat x n))) ;
|
||||
|
||||
--- data Elem = zero | succ ;
|
||||
|
||||
fun ex1 : Text ;
|
||||
def ex1 =
|
||||
ThmWithProof
|
||||
|
||||
@@ -17,13 +17,8 @@ WINDOWSINCLUDE =-ifor-windows $(BASICINCLUDE)
|
||||
DIST_DIR=GF-$(PACKAGE_VERSION)
|
||||
NOT_IN_DIST= \
|
||||
from-peb \
|
||||
doc/release2.html \
|
||||
grammars/resource \
|
||||
grammars/aggregation \
|
||||
grammars/numerals \
|
||||
grammars/ocl \
|
||||
grammars/testConversions \
|
||||
grammars/timetable \
|
||||
doc \
|
||||
grammars \
|
||||
src/parsing \
|
||||
src/conversions \
|
||||
src/util/AlphaConvGF.hs
|
||||
|
||||
Reference in New Issue
Block a user