Relación 1 - Historial de revisiones

Jalonso en 18:37 14 jul 2018

2018-07-14T18:37:50Z

Jospermon1 en 18:10 28 feb 2018

2018-02-28T18:10:02Z

Jalonso: Desprotegió «Relación 1»

2018-02-10T05:40:55Z

Desprotegió «Relación 1»

Jalonso en 14:56 2 nov 2017

2017-11-02T14:56:58Z

Jalonso: Protegió «Relación 1» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

2017-11-02T14:38:54Z

Protegió «Relación 1» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

Macmerflo en 13:04 2 nov 2017

2017-11-02T13:04:30Z

Davperriv en 11:44 2 nov 2017

2017-11-02T11:44:07Z

Davperriv en 11:40 2 nov 2017

2017-11-02T11:40:17Z

Davperriv en 11:35 2 nov 2017

2017-11-02T11:35:55Z

Davperriv en 11:29 2 nov 2017

2017-11-02T11:29:23Z

← Revisión anterior		Revisión del 18:37 14 jul 2018
Línea 1:		Línea 1:
−	<source lang="~~isar~~">	+	<source lang="isabelle">
	chapter {* R1: Programación funcional en Isabelle *}		chapter {* R1: Programación funcional en Isabelle *}

@@ Línea 41: / Línea 41: @@
 (* edupalhid anddonram cesgongut luicedval rafcabgon diwu2 jescudero
-    rafferrod davperriv macmerflo*)
+    rafferrod davperriv macmerflo jospermon1*)
 fun intercambia :: "'a × 'b ⇒ 'b × 'a" where
    "intercambia (x,y) = (y,x)"
@@ Línea 55: / Línea 55: @@
    ------------------------------------------------------------------ *}
-(* edupalhid cesgongut rafcabgon diwu2 jescudero*)
+(* edupalhid cesgongut rafcabgon diwu2 jescudero jospermon1*)
 fun inversa :: "'a list ⇒ 'a list" where
    "inversa [] = []" |
@@ Línea 105: / Línea 105: @@
 (* edupalhid anddonram cesgongut luicedval rafcabgon diwu2 rafferrod
-    davperriv macmerflo *)
+    davperriv macmerflo jospermon1*)
 fun repite :: "nat ⇒ 'a ⇒ 'a list" where
    "repite 0 x = []" |
@@ Línea 125: / Línea 125: @@
    ------------------------------------------------------------------ *}
-(* edupalhid anddonram cesgongut luicedval rafferrod macmerflo *)
+(* edupalhid anddonram cesgongut luicedval rafferrod macmerflo jospermon1*)
 fun conc :: "'a list ⇒ 'a list ⇒ 'a list" where
    "conc [] ys = ys" |
@@ Línea 189: / Línea 189: @@
 (* edupalhid anddonram cesgongut luicedval rafcabgon diwu2 rafferrod
-    jescudero macmerflo*)
+    jescudero macmerflo jospermon1*)
 fun elimina :: "nat ⇒ 'a list ⇒ 'a list" where
    "elimina 0 xs = xs" |
@@ Línea 277: / Línea 277: @@
 (* anddonram edupalhid cesgongut luicedval rafcabgon diwu2 rafferrod
-    jescudero macmerflo*)
+    jescudero macmerflo jospermon1*)
 fun sum :: "nat list ⇒ nat" where
    "sum [] = 0"
@@ Línea 298: / Línea 298: @@
 (* anddonram edupalhid cesgongut luicedval rafcabgon diwu2 rafferrod
-    jescudero macmerflo*)
+    jescudero macmerflo jospermon1*)
 fun map :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
    "map f [] = []"

@@ Línea 13: / Línea 13: @@
    ------------------------------------------------------------------- *}
-(* edupalhid anddonram jescudero cesgongut luicedval rafcabgon diwu2 jospermon1 macmerflo*)
+(* edupalhid anddonram jescudero cesgongut luicedval rafcabgon diwu2
 fun longitud :: "'a list ⇒ nat" where
    "longitud [] = 0" |
@@ Línea 24: / Línea 25: @@
 (* davperriv *)
-fun longitud :: "'a list ⇒ nat" where
+fun longitud3 :: "'a list ⇒ nat" where
-   "longitud [] = 0"
+   "longitud3 [] = 0"
-| "longitud xs = 1 + longitud (butlast xs)"
+| "longitud3 xs = 1 + longitud3 (butlast xs)"
 value "longitud [a,b,c] = 3"
@@ Línea 103: / Línea 104: @@
    ------------------------------------------------------------------ *}
-(* edupalhid anddonram cesgongut luicedval rafcabgon diwu2 rafferrod davperriv macmerflo *)
+(* edupalhid anddonram cesgongut luicedval rafcabgon diwu2 rafferrod
 fun repite :: "nat ⇒ 'a ⇒ 'a list" where
    "repite 0 x = []" |
@@ Línea 146: / Línea 148: @@
 (* davperriv *)
-fun conc :: "'a list ⇒ 'a list ⇒ 'a list" where
+fun conc4 :: "'a list ⇒ 'a list ⇒ 'a list" where
-   "conc [] ys = ys" |
+   "conc4 [] ys = ys" |
-   "conc xs ys = (hd xs) # conc (tl xs) ys"
+   "conc4 xs ys = (hd xs) # conc4 (tl xs) ys"
 text {* ---------------------------------------------------------------
@@ Línea 158: / Línea 160: @@
    ------------------------------------------------------------------ *}
-(* edupalhid anddonram cesgongut luicedval rafcabgon diwu2 rafferrod macmerflo *)
+(* edupalhid anddonram cesgongut luicedval rafcabgon diwu2
 fun coge :: "nat ⇒ 'a list ⇒ 'a list" where
    "coge n [] = []" |
@@ Línea 171: / Línea 174: @@
 (* davperriv *)
-fun coge :: "nat ⇒ 'a list ⇒ 'a list" where
+fun coge3 :: "nat ⇒ 'a list ⇒ 'a list" where
-   "coge 0 xs = []" |
+   "coge3 0 xs = []" |
-   "coge n xs = (hd xs) # coge (n-1) (tl xs)"
+   "coge3 n xs = (hd xs) # coge3 (n-1) (tl xs)"
 value "coge 2 [a,c,d,b,e] = [a,c]"
@@ Línea 195: / Línea 198: @@
 (* davperriv *)
-fun elimina :: "nat ⇒ 'a list ⇒ 'a list" where
+fun elimina2 :: "nat ⇒ 'a list ⇒ 'a list" where
-   "elimina 0 xs = xs" |
+   "elimina2 0 xs = xs" |
-   "elimina n xs = elimina (n-1) (tl xs)"
+   "elimina2 n xs = elimina2 (n-1) (tl xs)"
 text {* ---------------------------------------------------------------
@@ Línea 278: / Línea 281: @@
    "sum [] = 0"
   |"sum (x#xs) = x+sum xs"
 (* davperriv *)
-fun sum :: "nat list ⇒ nat" where
+fun sum2 :: "nat list ⇒ nat" where
-   "sum [] = 0" |
+   "sum2 [] = 0" |
-   "sum xs = (hd xs) + sum (tl xs)"
+   "sum2 xs = (hd xs) + sum2 (tl xs)"
 value "sum [3,2,5] = 10"
@@ Línea 302: / Línea 304: @@
 (* davperriv *)
-fun map :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
+fun map2 :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
-   "map f [] = []" |
+   "map2 f [] = []" |
-   "map f xs = f (hd xs) # map f (tl xs)"
+   "map2 f xs = f (hd xs) # map2 f (tl xs)"
 value "map (λx. x+1) [3::nat,2,4]=[4,3,5]"

@@ Línea 13: / Línea 13: @@
    ------------------------------------------------------------------- *}
-(* edupalhid anddonram jescudero cesgongut luicedval rafcabgon diwu2 jospermon1*)
+(* edupalhid anddonram jescudero cesgongut luicedval rafcabgon diwu2 jospermon1 macmerflo*)
 fun longitud :: "'a list ⇒ nat" where
    "longitud [] = 0" |
@@ Línea 40: / Línea 40: @@
 (* edupalhid anddonram cesgongut luicedval rafcabgon diwu2 jescudero
-    rafferrod davperriv*)
+    rafferrod davperriv macmerflo*)
 fun intercambia :: "'a × 'b ⇒ 'b × 'a" where
    "intercambia (x,y) = (y,x)"
@@ Línea 90: / Línea 90: @@
 value "inversa3 [a,d,c] = [c,d,a]"
-(* rafferrod davperriv *)
+(* rafferrod davperriv macmerflo *)
 fun inversa4 :: "'a list ⇒ 'a list" where
    "inversa4 [] = []" |
@@ Línea 103: / Línea 103: @@
    ------------------------------------------------------------------ *}
-(* edupalhid anddonram cesgongut luicedval rafcabgon diwu2 rafferrod davperriv *)
+(* edupalhid anddonram cesgongut luicedval rafcabgon diwu2 rafferrod davperriv macmerflo *)
 fun repite :: "nat ⇒ 'a ⇒ 'a list" where
    "repite 0 x = []" |
@@ Línea 123: / Línea 123: @@
    ------------------------------------------------------------------ *}
-(* edupalhid anddonram cesgongut luicedval rafferrod *)
+(* edupalhid anddonram cesgongut luicedval rafferrod macmerflo *)
 fun conc :: "'a list ⇒ 'a list ⇒ 'a list" where
    "conc [] ys = ys" |
@@ Línea 158: / Línea 158: @@
    ------------------------------------------------------------------ *}
-(* edupalhid anddonram cesgongut luicedval rafcabgon diwu2 rafferrod *)
+(* edupalhid anddonram cesgongut luicedval rafcabgon diwu2 rafferrod macmerflo *)
 fun coge :: "nat ⇒ 'a list ⇒ 'a list" where
    "coge n [] = []" |
@@ Línea 186: / Línea 186: @@
 (* edupalhid anddonram cesgongut luicedval rafcabgon diwu2 rafferrod
-    jescudero*)
+    jescudero macmerflo*)
 fun elimina :: "nat ⇒ 'a list ⇒ 'a list" where
    "elimina 0 xs = xs" |
@@ Línea 214: / Línea 214: @@
    "esVacia2 x = (x=[])"
-(* cesgongut luicedval rafcabgon rafferrod davperriv *)
+(* cesgongut luicedval rafcabgon rafferrod davperriv macmerflo*)
 fun esVacia3 :: "'a list ⇒ bool" where
    "esVacia3 [] = True" |
@@ Línea 274: / Línea 274: @@
 (* anddonram edupalhid cesgongut luicedval rafcabgon diwu2 rafferrod
-    jescudero*)
+    jescudero macmerflo*)
 fun sum :: "nat list ⇒ nat" where
    "sum [] = 0"
@@ Línea 296: / Línea 296: @@
 (* anddonram edupalhid cesgongut luicedval rafcabgon diwu2 rafferrod
-    jescudero*)
+    jescudero macmerflo*)
 fun map :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
    "map f [] = []"

@@ Línea 229: / Línea 229: @@
    ------------------------------------------------------------------ *}
-(* edupalhid anddonram rafcabgon diwu2 rafferrod *)
+(* edupalhid anddonram rafcabgon diwu2 rafferrod davperriv *)
 fun inversaAcAux :: "'a list ⇒ 'a list ⇒ 'a list" where
    "inversaAcAux [] ys = ys" |

← Revisión anterior	Revisión del 05:40 10 feb 2018
(Sin diferencias)

← Revisión anterior	Revisión del 14:38 2 nov 2017
(Sin diferencias)