Relación 1 - Historial de revisiones

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

2018-07-16T15:46:11Z

Texto reemplazado: «isar» por «isabelle»

Jalonso: Desprotegió «Relación 1»

2014-01-22T18:23:27Z

Desprotegió «Relación 1»

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

2013-12-07T07:56:08Z

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

Zoiruicha en 12:00 21 nov 2013

2013-11-21T12:00:40Z

Jaisalmen en 01:22 21 nov 2013

2013-11-21T01:22:25Z

Jaisalmen en 20:12 15 nov 2013

2013-11-15T20:12:44Z

Jaisalmen en 20:06 15 nov 2013

2013-11-15T20:06:18Z

Jaisalmen en 20:05 15 nov 2013

2013-11-15T20:05:33Z

Jaisalmen en 20:04 15 nov 2013

2013-11-15T20:04:41Z

Jaisalmen en 20:03 15 nov 2013

2013-11-15T20:03:03Z

← Revisión anterior		Revisión del 15:46 16 jul 2018
Línea 1:		Línea 1:
−	<source lang="~~isar~~">	+	<source lang="isabelle">

	header {* R1: Programación funcional en Isabelle *}		header {* R1: Programación funcional en Isabelle *}

@@ Línea 35: / Línea 35: @@
 value "factorial3 4" -- "24"
--- "jaisalmen"
+-- "jaisalmen zoiruicha"
 fun factorial4 :: "nat ⇒ nat" where
    "factorial4 0 = 1"
@@ Línea 77: / Línea 77: @@
 value "longitud4 [4,2,5]" -- "= 3"
--- ""jaisalmen"
+-- ""jaisalmen  zoiruicha"
 fun longitud5 :: "'a list ⇒ nat" where
    "longitud5 [] = 0"
@@ Línea 127: / Línea 127: @@
 value "inversa2 [a,d,c]" -- "= [c,d,a]"
--- "jaisalmen"
+-- "jaisalmen zoiruicha"
 fun inversa3 :: "'a list ⇒ 'a list" where
    "inversa3 [] = []"
@@ Línea 165: / Línea 165: @@
 value "repite3 3 a" -- "= [a,a,a]"
--- "domlloriv pabflomar jaisalmen"
+-- "domlloriv pabflomar jaisalmen zoiruicha"
 fun repite4 :: "nat ⇒ 'a ⇒ 'a list" where
    "repite4 0 x = []"
@@ Línea 208: / Línea 208: @@
 value "conc4 [a,d] [b,d,a,c]" -- "= [a,d,b,d,a,c]"
--- "jaisalmen"
+-- "jaisalmen zoiruicha"
 fun conc5 :: "'a list ⇒ 'a list ⇒ 'a list" where
    "conc5 [] ys = ys"
@@ Línea 259: / Línea 259: @@
 value "coge5 2 [a,c,d,b,e]" -- "= [a,c]"
--- "jaisalmen"
+-- "jaisalmen zoiruicha"
 fun coge6 :: "nat ⇒ 'a list ⇒ 'a list" where
    "coge6 0 xs = []"
@@ Línea 314: / Línea 314: @@
 value "elimina5 2 [a,c,d,b,e]"
--- "jaisalmen"
+-- "jaisalmen zoiruicha"
 fun elimina6 :: "nat ⇒ 'a list ⇒ 'a list" where
    "elimina6 0 xs = xs"
@@ Línea 354: / Línea 354: @@
 value "esVacia3 [1]" -- "= False"
--- "jaisalmen"
+-- "jaisalmen zoiruicha"
 fun esVacia4 :: "'a list ⇒ bool" where
    "esVacia4 x = (if longitud(x)=0 then True else False)"
@@ Línea 437: / Línea 437: @@
    ------------------------------------------------------------------ *}
--- "maresccas4 diecabmen1 domlloriv julrobrel juaruipav jaisalmen"
+-- "maresccas4 diecabmen1 domlloriv julrobrel juaruipav jaisalmen zoiruicha"
 fun sum :: "nat list ⇒ nat" where
    "sum []      = 0"
@@ Línea 488: / Línea 488: @@
 value "map4 (λx. 2*x) [3::nat,2,5]" -- "= [6,4,10]"
--- "jaisalmen"
+-- "jaisalmen zoiruicha"
 fun map :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
    "map5 f [] = []"

@@ Línea 127: / Línea 127: @@
 value "inversa2 [a,d,c]" -- "= [c,d,a]"
--- "jaisamen"
+-- "jaisalmen"
 fun inversa3 :: "'a list ⇒ 'a list" where
    "inversa3 [] = []"

← Revisión anterior		Revisión del 20:12 15 nov 2013
Línea 418:		Línea 418:

	value "inversaAc5 [a,c,b,e]" -- "= [e,b,c,a]"		value "inversaAc5 [a,c,b,e]" -- "= [e,b,c,a]"
		+
		+
		+	-- "jaisalmen"
		+	fun inverseAcAux6 :: "'a list ⇒ 'a list ⇒ 'a list" where
		+	"inverseAcAux6 xs ys = xs@ys"
		+
		+	fun inversaAc6 :: "'a list ⇒ 'a list" where
		+	"inversaAc6 [] = []"
		+	\| "inversaAc6 (x#xs) = inverseAcAux6 (inversaAc6 xs) [x]"
		+
		+	value "inversaAc6 [a,c,b,e]" -- "= [e,b,c,a]"

	text {* ---------------------------------------------------------------		text {* ---------------------------------------------------------------

@@ Línea 476: / Línea 476: @@
 value "map4 (λx. 2*x) [3::nat,2,5]" -- "= [6,4,10]"
 end
 </source>

← Revisión anterior	Revisión del 18:23 22 ene 2014
(Sin diferencias)

← Revisión anterior	Revisión del 07:56 7 dic 2013
(Sin diferencias)

@@ Línea 353: / Línea 353: @@
 value "esVacia3 []"  -- "= True"
 value "esVacia3 [1]" -- "= False"
 text {* ---------------------------------------------------------------

@@ Línea 265: / Línea 265: @@
 | "coge6 n (x#xs) = x # (coge6 (n-(1::nat)) xs)"
-value "coge 2 [a,c,d,b,e]" -- "= [a,c]"
+value "coge6 2 [a,c,d,b,e]" -- "= [a,c]"
@@ Línea 313: / Línea 313: @@
 value "elimina5 2 [a,c,d,b,e]"