Relación 1 - Historial de revisiones

Jalonso: Protegió «Relación 1» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

2019-03-06T18:48:35Z

Protegió «Relación 1» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

Jalonso en 13:03 28 feb 2019

2019-02-28T13:03:37Z

Jalonso en 10:48 28 feb 2019

2019-02-28T10:48:27Z

Alikan en 09:57 13 ene 2019

2019-01-13T09:57:34Z

Antramhur en 22:47 10 ene 2019

2019-01-10T22:47:46Z

Antramhur en 22:01 10 ene 2019

2019-01-10T22:01:40Z

Manperjim en 15:42 10 ene 2019

2019-01-10T15:42:09Z

Jalonso en 10:00 10 ene 2019

2019-01-10T10:00:24Z

Pabbergue en 14:12 30 dic 2018

2018-12-30T14:12:37Z

Alikan en 19:28 25 nov 2018

2018-11-25T19:28:40Z

@@ Línea 2: / Línea 2: @@
 chapter {* R1: Programación funcional en Isabelle *}
-theory R1_Programacion_funcional_en_Isabelle_alu
+theory R1_Programacion_funcional_en_Isabelle
 imports Main
 begin

@@ Línea 14: / Línea 14: @@
 (* cammonagu pabalagon raffergon2 aribatval juacanrod josgomrom4
-    marfruman1 gleherlop benber alfmarcua enrparlav manperjim chrgencar antramhur
+    marfruman1 gleherlop benber alfmarcua enrparlav manperjim chrgencar
-    pabbergue alikan*)
+    antramhur pabbergue alikan*)
 fun longitud :: "'a list ⇒ nat" where
    "longitud [] = 0 "
@@ Línea 37: / Línea 37: @@
    ------------------------------------------------------------------ *}
-(* manperjim pabalagon cammonagu raffergon2 aribatval juacanrod marfruman1
+(* manperjim pabalagon cammonagu raffergon2 aribatval juacanrod
-    gleherlop benber hugrubsan alfmarcua enrparalv giafus1 chrgencar
+    marfruman1 gleherlop benber hugrubsan alfmarcua enrparalv giafus1
-    antramhur alikan pabbergue *)
+    chrgencar antramhur alikan pabbergue *)
 fun intercambia :: "'a × 'b ⇒ 'b × 'a" where
    "intercambia (x,y) = (y, x)"
@@ Línea 110: / Línea 110: @@
    ------------------------------------------------------------------ *}
-(* pabalag aribatval antramhur*)
+(* pabalag aribatval antramhur *)
 fun repite :: "nat ⇒ 'a ⇒ 'a list" where
    "repite 0 x = []"
@@ Línea 117: / Línea 117: @@
 value "repite 3 a = [a,a,a]"
-(* manperjim raffergon2 cammonagu josgomrom4 marfruman1 benber alfmarcua gleherlop giafus1 chrgencar pabbergue alikan*)
+(* manperjim raffergon2 cammonagu josgomrom4 marfruman1 benber alfmarcua
 fun repite2 :: "nat ⇒ 'a ⇒ 'a list" where
    "repite2 0 x = [] "
@@ Línea 124: / Línea 125: @@
 value "repite2 3 a = [a,a,a]"
-(* juacanrod hugrubsan*)
+(* juacanrod hugrubsan *)
 fun repite3 :: "nat ⇒ 'a ⇒ 'a list" where
    "repite3 0 a = []"
@@ Línea 131: / Línea 132: @@
 value "repite3 3 a = [a,a,a]"
-(* enrparalv*)
+(* enrparalv *)
 fun repite4 :: "nat ⇒ 'a ⇒ 'a list" where
    "repite4 n x = (if n = 0 then [] else repite4 (n-1) x @ [x])"
@@ Línea 167: / Línea 168: @@
 value "conc3 [a,d] [b,d,a,c] = [a,d,b,d,a,c]"
-(* hugrubsan enrparalv giafus1 alikan*)
+(* hugrubsan enrparalv giafus1 alikan *)
 fun conc4 :: "'a list ⇒ 'a list ⇒ 'a list" where
    "conc4 xs ys = xs @ ys"
@@ Línea 246: / Línea 247: @@
 value "elimina 2 [a,c,d,b,e] = [d,b,e]"
-(* manperjim raffergon2 cammonagu josgomrom4 marfruman1 benber alfmarcua enrparalv
+(* manperjim raffergon2 cammonagu josgomrom4 marfruman1 benber alfmarcua
-    aribatval gleherlop chrgencar giafus1 pabbergue*)
+    enrparalv aribatval gleherlop chrgencar giafus1 pabbergue*)
 fun elimina2 :: "nat ⇒ 'a list ⇒ 'a list" where
    "elimina2 0 xs     = xs" |
@@ Línea 277: / Línea 278: @@
 (* manperjim pabalagon raffergon2 josgomrom4 marfruman1 benber hugrubsan
-    alfmarcua enrparalv aribatval chrgencar giafus1 alikan pabbergue antramhur *)
+    alfmarcua enrparalv aribatval chrgencar giafus1 alikan pabbergue
 fun esVacia :: "'a list ⇒ bool" where
    "esVacia [] = True" |
@@ Línea 299: / Línea 301: @@
 (* manperjim pabalagon cammonagu josgomrom4 marfruman1 benber alfmarcua
-    enrparalv aribatval gleherlop chrgencar giafus1 alikan pabbergue antramhur *)
+    enrparalv aribatval gleherlop chrgencar giafus1 alikan pabbergue
 fun inversaAcAux :: "'a list ⇒ 'a list ⇒ 'a list" where
    "inversaAcAux [] ys     = ys" |
@@ Línea 339: / Línea 342: @@
 (* manperjim pabalagon raffergon2 josgomrom4 marfruman1 benber alfmarcua
-    enrparalv aribatval gleherlop chrgencar giafus1 pabbergue antramhur alikan*)
+    enrparalv aribatval gleherlop chrgencar giafus1 pabbergue antramhur
 fun sum :: "nat list ⇒ nat" where
    "sum []     = 0" |

@@ Línea 15: / Línea 15: @@
 (* cammonagu pabalagon raffergon2 aribatval juacanrod josgomrom4
     marfruman1 gleherlop benber alfmarcua enrparlav manperjim chrgencar antramhur
-    pabbergue *)
+    pabbergue alikan*)
 fun longitud :: "'a list ⇒ nat" where
    "longitud [] = 0 "
@@ Línea 117: / Línea 117: @@
 value "repite 3 a = [a,a,a]"
-(* manperjim raffergon2 cammonagu josgomrom4 marfruman1 benber alfmarcua gleherlop giafus1 chrgencar pabbergue *)
+(* manperjim raffergon2 cammonagu josgomrom4 marfruman1 benber alfmarcua gleherlop giafus1 chrgencar pabbergue alikan*)
 fun repite2 :: "nat ⇒ 'a ⇒ 'a list" where
    "repite2 0 x = [] "
@@ Línea 339: / Línea 339: @@
 (* manperjim pabalagon raffergon2 josgomrom4 marfruman1 benber alfmarcua
-    enrparalv aribatval gleherlop chrgencar giafus1 pabbergue antramhur *)
+    enrparalv aribatval gleherlop chrgencar giafus1 pabbergue antramhur alikan*)
 fun sum :: "nat list ⇒ nat" where
    "sum []     = 0" |

@@ Línea 184: / Línea 184: @@
    ------------------------------------------------------------------ *}
-(* pabalagon raffergon2 *)
+(* pabalagon raffergon2 antramhur *)
 fun coge :: "nat ⇒ 'a list ⇒ 'a list" where
    "coge 0 xs           = []" |
@@ Línea 193: / Línea 193: @@
 (* manperjim cammonagu josgomrom4 marfruman1 benber alfmarcua chrgencar
-    gleherlop giafus1 pabbergue antramhur *)
+    gleherlop giafus1 pabbergue *)
 fun coge2 :: "nat ⇒ 'a list ⇒ 'a list" where
    "coge2 0 xs = []" |
@@ Línea 238: / Línea 238: @@
    ------------------------------------------------------------------ *}
-(* pabalagon *)
+(* pabalagon antramhur *)
 fun elimina :: "nat ⇒ 'a list ⇒ 'a list" where
    "elimina 0 xs           = []" |
@@ Línea 277: / Línea 277: @@
 (* manperjim pabalagon raffergon2 josgomrom4 marfruman1 benber hugrubsan
-    alfmarcua enrparalv aribatval chrgencar giafus1 alikan pabbergue *)
+    alfmarcua enrparalv aribatval chrgencar giafus1 alikan pabbergue antramhur *)
 fun esVacia :: "'a list ⇒ bool" where
    "esVacia [] = True" |
@@ Línea 299: / Línea 299: @@
 (* manperjim pabalagon cammonagu josgomrom4 marfruman1 benber alfmarcua
-    enrparalv aribatval gleherlop chrgencar giafus1 alikan pabbergue *)
+    enrparalv aribatval gleherlop chrgencar giafus1 alikan pabbergue antramhur *)
 fun inversaAcAux :: "'a list ⇒ 'a list ⇒ 'a list" where
    "inversaAcAux [] ys     = ys" |
@@ Línea 339: / Línea 339: @@
 (* manperjim pabalagon raffergon2 josgomrom4 marfruman1 benber alfmarcua
-    enrparalv aribatval gleherlop chrgencar giafus1 pabbergue *)
+    enrparalv aribatval gleherlop chrgencar giafus1 pabbergue antramhur *)
 fun sum :: "nat list ⇒ nat" where
    "sum []     = 0" |
@@ Línea 370: / Línea 370: @@
 (* manperjim pabalagon raffergon2 cammonagu josgomrom4 marfruman1 benber
-    alfmarcua aribatval gleherlop chrgencar giafus1 pabbergue *)
+    alfmarcua aribatval gleherlop chrgencar giafus1 pabbergue antramhur *)
 fun map :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
    "map f []     = []" |

@@ Línea 146: / Línea 146: @@
 (* manperjim pabalagon raffergon2 josgomrom4 aribatval gleherlop
-    chrgencar benber *)
+    chrgencar benber antramhur*)
 fun conc :: "'a list ⇒ 'a list ⇒ 'a list" where
    "conc [] ys     = ys" |
@@ Línea 193: / Línea 193: @@
 (* manperjim cammonagu josgomrom4 marfruman1 benber alfmarcua chrgencar
-    gleherlop giafus1 pabbergue *)
+    gleherlop giafus1 pabbergue antramhur *)
 fun coge2 :: "nat ⇒ 'a list ⇒ 'a list" where
    "coge2 0 xs = []" |

← Revisión anterior	Revisión del 18:48 6 mar 2019
(Sin diferencias)

@@ Línea 14: / Línea 14: @@
 (* manperjim cammonagu pabalagon raffergon2 aribatval juacanrod josgomrom4
-    marfruman1 gleherlop benber alfmarcua enrparlav chrgencar antramhur pabbergue *)
+    marfruman1 gleherlop benber alfmarcua enrparlav chrgencar antramhur
 fun longitud :: "'a list ⇒ nat" where
    "longitud [] = 0 "
@@ Línea 37: / Línea 38: @@
 (* manperjim pabalagon cammonagu raffergon2 aribatval juacanrod marfruman1
-    gleherlop benber hugrubsan alfmarcua enrparalv giafus1 chrgencar antramhur alikan pabbergue *)
+    gleherlop benber hugrubsan alfmarcua enrparalv giafus1 chrgencar
 fun intercambia :: "'a × 'b ⇒ 'b × 'a" where
    "intercambia (x,y) = (y, x)"
@@ Línea 67: / Línea 69: @@
 value "inversa [a,d,c] = [c,d,a]"
-(* manperjim pabalagon raffergon2 cammonagu josgomrom4 marfruman1 gleherlop
+(* manperjim pabalagon raffergon2 cammonagu josgomrom4 marfruman1
-    alfmarcua enrparalv chrgencar antramhur alikan pabbergue *)
+    gleherlop alfmarcua enrparalv chrgencar antramhur alikan pabbergue *)
 fun inversa2 :: "'a list ⇒ 'a list" where
-   "inversa2 [] = []"
+   "inversa2 []     = []"
 | "inversa2 (x#xs) = inversa2 xs @ [x]"
@@ Línea 77: / Línea 79: @@
 (* juacanrod hugrubsan giafus1 *)
 fun inversa3 :: "'a list ⇒ 'a list" where
-   "inversa3 [] = []"
+   "inversa3 []   = []"
 | "inversa3 (xs) = inversa3(tl xs) @ [ hd (xs)]"
@@ Línea 143: / Línea 145: @@
    ------------------------------------------------------------------ *}
-(* manperjim pabalagon raffergon2 josgomrom4 aribatval gleherlop chrgencar benber *)
+(* manperjim pabalagon raffergon2 josgomrom4 aribatval gleherlop
 fun conc :: "'a list ⇒ 'a list ⇒ 'a list" where
    "conc [] ys     = ys" |
@@ Línea 189: / Línea 192: @@
 value "coge 2 [a,c,d,b,e] = [a,c]"
-(* manperjim cammonagu josgomrom4 marfruman1 benber alfmarcua chrgencar gleherlop giafus1 pabbergue *)
+(* manperjim cammonagu josgomrom4 marfruman1 benber alfmarcua chrgencar
 fun coge2 :: "nat ⇒ 'a list ⇒ 'a list" where
    "coge2 0 xs = []" |
@@ Línea 215: / Línea 219: @@
 fun coge5 :: "nat ⇒ 'a list ⇒ 'a list" where
    "coge5 n []      = []"
-  |"coge5 n (x#xs) = (if (n=0) then [] else [x] @ coge5 (n-1) xs )"
+| "coge5 n (x#xs) = (if (n=0) then [] else [x] @ coge5 (n-1) xs )"
 value "coge5 2 [a,c,d,b,e] = [a,c]"
@@ Línea 272: / Línea 276: @@
    ------------------------------------------------------------------ *}
-(* manperjim pabalagon raffergon2 josgomrom4 marfruman1 benber hugrubsan alfmarcua
+(* manperjim pabalagon raffergon2 josgomrom4 marfruman1 benber hugrubsan
-    enrparalv aribatval chrgencar giafus1 alikan pabbergue*)
+    alfmarcua enrparalv aribatval chrgencar giafus1 alikan pabbergue *)
 fun esVacia :: "'a list ⇒ bool" where
    "esVacia [] = True" |
@@ Línea 294: / Línea 298: @@
    ------------------------------------------------------------------ *}
-(* manperjim pabalagon cammonagu josgomrom4 marfruman1 benber alfmarcua enrparalv aribatval gleherlop chrgencar giafus1 alikan pabbergue *)
+(* manperjim pabalagon cammonagu josgomrom4 marfruman1 benber alfmarcua
 fun inversaAcAux :: "'a list ⇒ 'a list ⇒ 'a list" where
    "inversaAcAux [] ys     = ys" |
@@ Línea 333: / Línea 338: @@
    ------------------------------------------------------------------ *}
-(* manperjim pabalagon raffergon2 josgomrom4 marfruman1 benber alfmarcua enrparalv aribatval gleherlop chrgencar giafus1 pabbergue*)
+(* manperjim pabalagon raffergon2 josgomrom4 marfruman1 benber alfmarcua
 fun sum :: "nat list ⇒ nat" where
    "sum []     = 0" |
@@ Línea 363: / Línea 369: @@
    ------------------------------------------------------------------ *}
-(* manperjim pabalagon raffergon2 cammonagu josgomrom4 marfruman1 benber alfmarcua
+(* manperjim pabalagon raffergon2 cammonagu josgomrom4 marfruman1 benber
-    aribatval gleherlop chrgencar giafus1 pabbergue *)
+    alfmarcua aribatval gleherlop chrgencar giafus1 pabbergue *)
 fun map :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
    "map f []     = []" |