gfcm header

2 files changed, 16 insertions, 8 deletions

diff --git a/grammars/logic/Arithm.gf b/grammars/logic/Arithm.gf
index 2d2e12fd9..2a91c5ed0 100644
--- a/grammars/logic/Arithm.gf
+++ b/grammars/logic/Arithm.gf
@@ -3,9 +3,10 @@ abstract Arithm = Logic ** {
 -- arithmetic
 fun 
   Nat, Real  : Dom ;
+data
   zero : Elem Nat ;
   succ : Elem Nat -> Elem Nat ;
-  
+fun
   trunc : Elem Real -> Elem Nat ;
 
   EqNat : (m,n : Elem Nat) -> Prop ;
@@ -19,13 +20,13 @@ fun
   two  : Elem Nat ;
   sum  : (m,n : Elem Nat) -> Elem Nat ;
   prod : (m,n : Elem Nat) -> Elem Nat ;
-
+data
   evax1 : Proof (Even zero) ;
   evax2 : (n : Elem Nat) -> Proof (Even n) -> Proof (Odd (succ n)) ;
   evax3 : (n : Elem Nat) -> Proof (Odd n)  -> Proof (Even (succ n)) ;
   eqax1 : Proof (EqNat zero zero) ;
   eqax2 : (m,n : Elem Nat) -> Proof (EqNat m n) -> Proof (EqNat (succ m) (succ n)) ;
-
+fun
   IndNat : (C : Elem Nat -> Prop) -> 
              Proof (C zero) -> 
              ((x : Elem Nat) -> Proof (C x) -> Proof (C (succ x))) -> 
@@ -45,7 +46,6 @@ def
               (Univ Nat (\x -> Impl (Conj (LtNat one x) (Div n x)) (EqNat x n))) ;
 
   Abs = Abs ;
----  data Elem = zero | succ ;
 
 fun ex1 : Text ;
 def ex1 = 
diff --git a/grammars/logic/Logic.gf b/grammars/logic/Logic.gf
index 3e2516ebc..41fd5cef8 100644
--- a/grammars/logic/Logic.gf
+++ b/grammars/logic/Logic.gf
@@ -32,25 +32,36 @@ fun
   ImplP : (A : Prop) -> (Proof A -> Prop) -> Prop ;
 
   -- inference rules
+data  
   ConjI  : (A,B : Prop) -> Proof A -> Proof B -> Proof (Conj A B) ;
+fun  
   ConjEl : (A,B : Prop) -> Proof (Conj A B) -> Proof A ;
   ConjEr : (A,B : Prop) -> Proof (Conj A B) -> Proof B ;
+data  
   DisjIl : (A,B : Prop) -> Proof A -> Proof (Disj A B) ;
   DisjIr : (A,B : Prop) -> Proof B -> Proof (Disj A B) ;
+fun  
   DisjE  : (A,B,C : Prop) -> Proof (Disj A B) -> 
               (Proof A -> Proof C) -> (Proof B -> Proof C) -> Proof C ;
+data
   ImplI  : (A,B : Prop) -> (Proof A -> Proof B) -> Proof (Impl A B) ;
+fun
   ImplE  : (A,B : Prop) -> Proof (Impl A B) -> Proof A -> Proof B ;
+data
   NegI   : (A : Prop) -> (Proof A -> Proof Abs) -> Proof (Neg A) ;
+fun
   NegE   : (A : Prop) -> Proof (Neg A) -> Proof A -> Proof Abs ;
   AbsE   : (C : Prop) -> Proof Abs -> Proof C ;
-
+data
   UnivI  : (A : Dom) -> (B : Elem A -> Prop) -> 
               ((x : Elem A) -> Proof (B x)) -> Proof (Univ A B) ;
+fun
   UnivE  : (A : Dom) -> (B : Elem A -> Prop) -> 
               Proof (Univ A B) -> (a : Elem A) -> Proof (B a) ;
+data
   ExistI : (A : Dom) -> (B : Elem A -> Prop) -> 
               (a : Elem A) -> Proof (B a) -> Proof (Exist A B) ;
+fun
   ExistE : (A : Dom) -> (B : Elem A -> Prop) -> (C : Prop) -> 
               Proof (Exist A B) -> ((x : Elem A) -> Proof (B x) -> Proof C) -> 
               Proof C ;
@@ -61,9 +72,6 @@ fun
   -- pronoun
   Pron : (A : Dom) -> Elem A -> Elem A ;
 
-data
-  Proof = ConjI | DisjIl | DisjIr ;
-
 def 
   -- proof normalization
   ConjEl _ _ (ConjI _ _ a _) = a ;