French logic

1 files changed, 37 insertions, 0 deletions

diff --git a/grammars/logic/ArithmFre.gf b/grammars/logic/ArithmFre.gf
new file mode 100644
index 000000000..fcc99f4e9
--- /dev/null
+++ b/grammars/logic/ArithmFre.gf
@@ -0,0 +1,37 @@
+--# -path=.:../prelude
+
+concrete ArithmFre of Arithm = LogicFre ** open ResFre in {
+
+lin Nat = {g = masc ; s = nomReg "nombre"} ;
+zero = {g = masc ; s = table {c => (prep ! c) ++ "zéro"}} ;
+succ n =
+  {g = masc ; s = table {c => defin ! sg ! masc ! c ++ "successeur" ++ n.s ! dd}} ;
+EqNat k n = mkPropA2 aa k (adjAl "éga") n ;
+LtNat k n = mkPropA2 aa k (adjReg "inférieur") n ;
+Div k n = mkPropA2 nom k (table {_ => nomReg "divisible"}) n ; --- par !
+
+Even n = mkPropA1 n (adjReg "pair") ;
+Odd n = mkPropA1 n (adjReg "impair") ;
+Prime n = mkPropA1 n (adjEr "premi") ;
+
+lin one  =
+  {g = masc ; s = table {c => (prep ! c) ++ "un"}} ;
+lin two  =
+  {g = masc ; s = table {c => (prep ! c) ++ "deux"}} ;
+lin sum m n = {g = fem ; s = table {
+  c => defin ! sg ! fem ! c ++ "somme" ++ m.s ! dd ++ "et" ++ n.s ! dd}} ;
+lin prod m n = {g = masc ; s = table {
+  c => defin!sg!fem!c ++ "produit" ++ m.s ! dd ++ "et" ++ n.s ! dd}} ;
+lin evax1  =
+  {s = "par"++"le"++"premier"++"axiome"++"de"++"parité,"++"zéro"++"est"++"pair"} ;
+lin evax2 n c =
+  {s = c.s ++ "."++"Par"++"le"++"deuxième"++"axiome"++"de"++"parité,"++"le"++"successeur" ++ (n.s ! dd) ++ "est"++"impair"} ;
+lin evax3 n c =
+  {s = c.s ++ "."++"Par"++"le"++"troisième"++"axiome"++"de"++"parité,"++"le"++"successeur" ++ (n.s ! dd) ++ "est"++"pair"} ;
+lin eqax1  =
+  {s = "par"++"le"++"premier"++"axiome"++"d'égalité,"++"zéro"++"est"++"égal"++"a"++"lui-même"} ;
+lin eqax2 m n c =
+  {s = c.s ++ "."++"Par"++"le"++"deuxième"++"axiome"++"d'égalité,"++"le"++"successeur" ++ (m.s ! dd) ++ "est"++"égal"++"au"++"successeur" ++ n.s ! dd} ;
+lin IndNat C d e =
+  {s = "nous"++"nous"++"servons"++"d'induction."++"Pour"++"la"++"base," ++ d.s ++ "."++"Pour"++"le"++"pas"++"d'induction,"++"considérons"++"un"++"nombre" ++ e.$0 ++ "et"++"supposons" ++ que ++ (C.s ! ind) ++ "(" ++ e.$1 ++ ")" ++ "." ++ e.s ++ "Donc,"++"pour"++"tous"++"les"++"nombres" ++ C.$0 ++ "," ++ C.s ! ind} ;
+}