Relación 1 - Historial de revisiones

WikiSysop: Texto reemplazado: «isar» por «isabelle»

2018-07-16T11:11:18Z

Texto reemplazado: «isar» por «isabelle»

Juacabsou en 12:33 12 feb 2017

2017-02-12T12:33:57Z

Fracorjim1 en 12:04 5 ene 2017

2017-01-05T12:04:44Z

Fracorjim1 en 11:59 5 ene 2017

2017-01-05T11:59:42Z

Fracorjim1 en 11:49 5 ene 2017

2017-01-05T11:49:39Z

Antsancab1 en 20:06 9 dic 2016

2016-12-09T20:06:41Z

Jalonso: Desprotegió «Relación 1»

2016-12-08T17:45:43Z

Desprotegió «Relación 1»

Jalonso: Cambió el nivel de protección de «Relación 1» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

2016-11-09T15:27:35Z

Cambió el nivel de protección de «Relación 1» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

Jalonso en 15:27 9 nov 2016

2016-11-09T15:27:14Z

Jalonso: Protegió «Relación 1» ([edit=sysop] (caduca el 16:12 9 nov 2016 (UTC)) [move=sysop] (caduca el 16:12 9 nov 2016 (UTC)))

2016-11-09T15:12:13Z

Protegió «Relación 1» ([edit=sysop] (caduca el 16:12 9 nov 2016 (UTC)) [move=sysop] (caduca el 16:12 9 nov 2016 (UTC)))

← Revisión anterior		Revisión del 11:11 16 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 14: / Línea 14: @@
 (* danrodcha anaprarod ivamenjim serrodcal manmorjim1 fraortmoy
-    dancorgar ferrenseg paupeddeg pabrodmac antsancab1 fracorjim1 *)
+    dancorgar ferrenseg paupeddeg pabrodmac antsancab1 fracorjim1 juacabsou *)
 fun factorial :: "nat ⇒ nat" where
    "factorial 0 = 1"
@@ Línea 43: / Línea 43: @@
 (* wilmorort serrodcal crigomgom rubgonmar anaprarod dancorgar ferrenseg
-    paupeddeg pabrodmac antsancab1 *)
+    paupeddeg pabrodmac antsancab1 juacabsou *)
 fun longitud :: "'a  list  ⇒ nat" where
    "longitud []       = 0" |
@@ Línea 105: / Línea 105: @@
 (* wilmorort marcarmor13 danrodcha crigomgom pablucoto rubgonmar
     manmorjim1 serrodcal fraortmoy anaprarod dancorgar ferrenseg
-    paupeddeg pabrodmac antsancab1 fracorjim1 *)
+    paupeddeg pabrodmac antsancab1 fracorjim1 juacabsou*)
 fun intercambia :: "'a × 'b ⇒ 'b × 'a" where
    "intercambia (x,y) = (y,x)"
@@ Línea 157: / Línea 157: @@
 value "inversa3 [a,d,c] = [c,d,a]"
-(* crigomgom serrodcal marpoldia1*)
+(* crigomgom serrodcal marpoldia1 juacabsou *)
 fun inversa4 :: "'a list ⇒ 'a list" where
    "inversa4 [] = []" |
@@ Línea 181: / Línea 181: @@
 (* wilmorort marcarmor13 crigomgom pablucoto rubgonmar manmorjim1
-    jeamacpov ivamenjim marpoldia1*)
+    jeamacpov ivamenjim marpoldia1 juacabsou *)
 fun repite :: "nat ⇒ 'a ⇒ 'a list" where
    "repite 0 x = [] " |
@@ Línea 235: / Línea 235: @@
 value "conc1 [a,d] [b,d,a,c] = [a,d,b,d,a,c]"
-(* pablucoto jeamacpov fraortmoy anaprarod ferrenseg pabrodmac antsancab1 fracorjim1 *)
+(* pablucoto jeamacpov fraortmoy anaprarod ferrenseg pabrodmac antsancab1 fracorjim1 juacabsou *)
 fun conc2 :: "'a list ⇒ 'a list ⇒ 'a list" where
    "conc2 [] ys     = ys" |
@@ Línea 294: / Línea 294: @@
 value "coge 2 [a,c,d,b,e] = [a,c]"
-(* danrodcha fraortmoy anaprarod ferrenseg paupeddeg pabrodmac *)
+(* danrodcha fraortmoy anaprarod ferrenseg paupeddeg pabrodmac juacabsou *)
 fun coge1 :: "nat ⇒ 'a list ⇒ 'a list" where
    "coge1 0 _            = []"
@@ Línea 373: / Línea 373: @@
 | "elimina n xs = (elimina (n-1) (tl xs ))"
-(* danrodcha crigomgom fraortmoy anaprarod paupeddeg pabrodmac *)
+(* danrodcha crigomgom fraortmoy anaprarod paupeddeg pabrodmac juacabsou *)
 fun elimina1 :: "nat ⇒ 'a list ⇒ 'a list" where
    "elimina1 0 xs           = xs"
@@ Línea 462: / Línea 462: @@
 value "esVacia4 [1] = False"
-(* ferrenseg fracorjim1 *)
+(* ferrenseg fracorjim1 juacabsou *)
 fun esVacia5 :: "'a list ⇒ bool" where
    "esVacia5 [] = True"
@@ Línea 498: / Línea 498: @@
 value "inversaAc [a,c,b,e]= [e,b,c,a]"
-(* danrodcha crigomgom anaprarod paupeddeg *)
+(* danrodcha crigomgom anaprarod paupeddeg juacabsou *)
 fun inversaAcAux1 :: "'a list ⇒ 'a list ⇒ 'a list" where
    "inversaAcAux1 [] ys     = ys"
@@ Línea 583: / Línea 583: @@
 (* danrodcha crigomgom pablucoto fraortmoy anaprarod ferrenseg paupeddeg
-    pabrodmac antsancab1 fracorjim1 *)
+    pabrodmac antsancab1 fracorjim1 juacabsou *)
 fun sum1 :: "nat list ⇒ nat" where
    "sum1 []     = 0"
@@ Línea 633: / Línea 633: @@
 (* wilmorort danrodcha crigomgom pablucoto fraortmoy anaprarod dancorgar
-    ferrenseg paupeddeg pabrodmac antsancab1 fracorjim1 *)
+    ferrenseg paupeddeg pabrodmac antsancab1 fracorjim1 juacabsou *)
 fun map2 :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
    "map2 f [] = []"

@@ Línea 462: / Línea 462: @@
 value "esVacia4 [1] = False"
-(* ferrenseg *)
+(* ferrenseg fracorjim1 *)
 fun esVacia5 :: "'a list ⇒ bool" where
    "esVacia5 [] = True"
@@ Línea 583: / Línea 583: @@
 (* danrodcha crigomgom pablucoto fraortmoy anaprarod ferrenseg paupeddeg
-    pabrodmac antsancab1 *)
+    pabrodmac antsancab1 fracorjim1 *)
 fun sum1 :: "nat list ⇒ nat" where
    "sum1 []     = 0"
@@ Línea 633: / Línea 633: @@
 (* wilmorort danrodcha crigomgom pablucoto fraortmoy anaprarod dancorgar
-    ferrenseg paupeddeg pabrodmac antsancab1 *)
+    ferrenseg paupeddeg pabrodmac antsancab1 fracorjim1 *)
 fun map2 :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
    "map2 f [] = []"

@@ Línea 188: / Línea 188: @@
 value "repite 3 a = [a,a,a]"
-(* danrodcha fraortmoy dancorgar ferrenseg paupeddeg pabrodmac antsancab1 *)
+(* danrodcha fraortmoy dancorgar ferrenseg paupeddeg pabrodmac antsancab1 fracorjim1 *)
 fun repite1 :: "nat ⇒ 'a ⇒ 'a list" where
    "repite1 0 x       = []"
@@ Línea 235: / Línea 235: @@
 value "conc1 [a,d] [b,d,a,c] = [a,d,b,d,a,c]"
-(* pablucoto jeamacpov fraortmoy anaprarod ferrenseg pabrodmac antsancab1 *)
+(* pablucoto jeamacpov fraortmoy anaprarod ferrenseg pabrodmac antsancab1 fracorjim1 *)
 fun conc2 :: "'a list ⇒ 'a list ⇒ 'a list" where
    "conc2 [] ys     = ys" |
@@ Línea 354: / Línea 354: @@
 value "coge7 2 [] = []"
 value "coge7 2 [a,c,d,b,e] = [a,c]"
 text {* ---------------------------------------------------------------
@@ Línea 411: / Línea 416: @@
 value "elimina6 2 [a,c,d,b,e]" -- "= [d,b,e]"
 text {* ---------------------------------------------------------------

@@ Línea 14: / Línea 14: @@
 (* danrodcha anaprarod ivamenjim serrodcal manmorjim1 fraortmoy
-    dancorgar ferrenseg paupeddeg pabrodmac antsancab1 *)
+    dancorgar ferrenseg paupeddeg pabrodmac antsancab1 fracorjim1 *)
 fun factorial :: "nat ⇒ nat" where
    "factorial 0 = 1"
@@ Línea 72: / Línea 72: @@
 value "longitud4 [4,2,5] = 3"
-(* danrodcha *)
+(* danrodcha fracorjim1 *)
 fun longitud5 :: "'a list ⇒ nat" where
    "longitud5 []     = 0"
@@ Línea 105: / Línea 105: @@
 (* wilmorort marcarmor13 danrodcha crigomgom pablucoto rubgonmar
     manmorjim1 serrodcal fraortmoy anaprarod dancorgar ferrenseg
-    paupeddeg pabrodmac antsancab1 *)
+    paupeddeg pabrodmac antsancab1 fracorjim1 *)
 fun intercambia :: "'a × 'b ⇒ 'b × 'a" where
    "intercambia (x,y) = (y,x)"
@@ Línea 142: / Línea 142: @@
 (* danrodcha pablucoto rubgonmar anaprarod dancorgar ferrenseg paupeddeg
-    pabrodmac *)
+    pabrodmac fracorjim1 *)
 (* es igual que inversa sustituyendo x#[] por [x] *)
 fun inversa2 :: "'a list ⇒ 'a list" where

← Revisión anterior	Revisión del 17:45 8 dic 2016
(Sin diferencias)

← Revisión anterior	Revisión del 15:27 9 nov 2016
(Sin diferencias)

@@ Línea 13: / Línea 13: @@
    ------------------------------------------------------------------- *}
-(* danrodcha anaprarod ivamenjim serrodcal manmorjim1 fraortmoy dancorgar ferrenseg paupeddeg pabrodmac*)
+(* danrodcha anaprarod ivamenjim serrodcal manmorjim1 fraortmoy
 fun factorial :: "nat ⇒ nat" where
    "factorial 0 = 1"
@@ Línea 41: / Línea 42: @@
    "[x]" == "x#[]"
-(* wilmorort serrodcal crigomgom rubgonmar anaprarod dancorgar ferrenseg paupeddeg pabrodmac*)
+(* wilmorort serrodcal crigomgom rubgonmar anaprarod dancorgar ferrenseg
 fun longitud :: "'a  list  ⇒ nat" where
    "longitud []       = 0" |
@@ Línea 102: / Línea 104: @@
 (* wilmorort marcarmor13 danrodcha crigomgom pablucoto rubgonmar
-    manmorjim1 serrodcal fraortmoy anaprarod dancorgar ferrenseg paupeddeg pabrodmac *)
+    manmorjim1 serrodcal fraortmoy anaprarod dancorgar ferrenseg
 fun intercambia :: "'a × 'b ⇒ 'b × 'a" where
    "intercambia (x,y) = (y,x)"
@@ Línea 138: / Línea 141: @@
 value "inversa1 [a,d,c] = [c,d,a]"
-(* danrodcha pablucoto rubgonmar anaprarod dancorgar ferrenseg paupeddeg pabrodmac *)
+(* danrodcha pablucoto rubgonmar anaprarod dancorgar ferrenseg paupeddeg
 (* es igual que inversa sustituyendo x#[] por [x] *)
 fun inversa2 :: "'a list ⇒ 'a list" where
@@ Línea 260: / Línea 264: @@
 value "conc5 [a,d] [b,d,a,c] = [a,d,b,d,a,c]"
 (* marpoldia1 *)
 fun conc6 :: "'a list ⇒ 'a list ⇒ 'a list" where
- "conc6 [] [] = []"|
+  "conc6 [] [] = []"
- "conc6 [] ys = ys"|
+| "conc6 [] ys = ys"
- "conc6 xs ys = (hd xs)#(conc6 (tl xs) ys)"
+| "conc6 xs ys = (hd xs)#(conc6 (tl xs) ys)"
 value "conc6 [a,d] [b,d,a,c] = [a,d,b,d,a,c]"
 text {* ---------------------------------------------------------------
@@ Línea 411: / Línea 420: @@
    ------------------------------------------------------------------ *}
-(* marcarmor13 rubgonmar danrodcha crigomgom fraortmoy dancorgar paupeddeg *)
+(* marcarmor13 rubgonmar danrodcha crigomgom fraortmoy dancorgar
 fun esVacia :: "'a list ⇒ bool" where
    "esVacia [] = True "
@@ Línea 443: / Línea 453: @@
 (* ferrenseg *)
 fun esVacia5 :: "'a list ⇒ bool" where
    "esVacia5 [] = True"
@@ Línea 452: / Línea 461: @@
 (* pabrodmac *)
 fun esVacia6 :: "'a list ⇒ bool" where
    "esVacia6 [] = True"
@@ Línea 473: / Línea 481: @@
 | "inversaAcAux xs ys = inversaAcAux (tl xs) (hd xs#ys) "
-(* rubgonmar danrodcha crigomgom manmorjim1 serrodcal ivamenjim anaprarod marpoldia1*)
+(* rubgonmar danrodcha crigomgom manmorjim1 serrodcal ivamenjim
 fun inversaAc :: "'a list ⇒ 'a list" where
    "inversaAc xs = inversaAcAux xs []"
@@ Línea 503: / Línea 512: @@
 value "inversaAc3 [a,c,b,e]= [e,b,c,a]"
 (* fraortmoy *)
 fun inversaAcAux4 :: "'a list ⇒ 'a list ⇒ 'a list" where
    "inversaAcAux4 xs [] = xs"
@@ Línea 529: / Línea 536: @@
 value "inversaAc5 [a,c,b,e] = [e,b,c,a]" -- "= [e,b,c,a]"
 (* ferrenseg *)
 fun inversaAcAux6 :: "'a list ⇒ 'a list ⇒ 'a list" where
    "inversaAcAux6 [] ys = ys"
@@ Línea 543: / Línea 548: @@
 (* pabrodmac *)
 fun inversaAcAux7 :: "'a list ⇒ 'a list ⇒ 'a list" where
    "inversaAcAux7 [] ys = ys "
@@ Línea 568: / Línea 572: @@
 value "sum [3,2,5] = 10"
-(* danrodcha crigomgom pablucoto fraortmoy anaprarod ferrenseg paupeddeg pabrodmac *)
+(* danrodcha crigomgom pablucoto fraortmoy anaprarod ferrenseg paupeddeg
 fun sum1 :: "nat list ⇒ nat" where
    "sum1 []     = 0"
@@ Línea 617: / Línea 622: @@
 value "map (λx. 2*x) [3::nat,2,5] = [6,4,10]"
-(* wilmorort danrodcha crigomgom pablucoto fraortmoy anaprarod dancorgar ferrenseg paupeddeg pabrodmac *)
+(* wilmorort danrodcha crigomgom pablucoto fraortmoy anaprarod dancorgar
 fun map2 :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
    "map2 f [] = []"

← Revisión anterior	Revisión del 15:12 9 nov 2016
(Sin diferencias)