GitHub/gf-core
1
0
Fork 1
mirror of https://github.com/GrammaticalFramework/gf-core.git synced 2026-05-07 02:02:51 -06:00
Code Issues Packages Projects Releases Wiki Activity

small adjustments in grs

Browse Source
This commit is contained in:
aarne
2004-08-09 13:22:59 +00:00
parent 466ab5db4e
commit 046a13ce7e
4 changed files with 15 additions and 13 deletions
Download Patch File Download Diff File Expand all files Collapse all files

6
grammars/logic/Arithm.gf
View File

@@ -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