diff options
| -rw-r--r-- | grammars/logic/Arithm.gf | 6 | ||||
| -rw-r--r-- | src/Makefile | 9 |
2 files changed, 6 insertions, 9 deletions
diff --git a/grammars/logic/Arithm.gf b/grammars/logic/Arithm.gf index e3ae706a4..7674e9551 100644 --- a/grammars/logic/Arithm.gf +++ b/grammars/logic/Arithm.gf @@ -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 diff --git a/src/Makefile b/src/Makefile index cc90f582f..1d3814a6a 100644 --- a/src/Makefile +++ b/src/Makefile @@ -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 |