rewrite.idris 的修订

1 file changed, 0 insertions, 0 deletions

rewrite.idris 重命名为 rewrite.idr

文件已重命名，但内容与之前没有差异

1 file changed, 25 insertions

rewrite.idris(文件已创建)

		@@ -0,0 +1,25 @@
1	+	rewrite : (default : List String) ->
2	+	(apples : List String) ->
3	+	(oranges : List String) ->
4	+	(cherries : List String) ->
5	+	(fruit_salad : List String) ->
6	+	(bowl : List String) ->
7	+	List (List String)
8	+
9	+	rewrite default ([] :: apples) ([] :: oranges) ([] :: cherries) fruit_salad bowl =
10	+	rewrite default apples oranges cherries ([] :: fruitSalad) bowl
11	+
12	+	rewrite default apples oranges cherries fruit_salad bowl =
13	+	rewrite
14	+	( ["add", "apples", "to", "the", "bowl"]
15	+	:: ["add", "oranges", "to", "the", "bowl"]
16	+	:: ["add", "cherries", "to", "the", "bowl"]
17	+	:: default )
18	+	apples oranges cherries fruit_salad bowl
19	+
20	+	rewrite (["add", x, "to", "the", "bowl"] :: defualt)
21	+	apples oranges cherries fruit_salad bowl =
22	+	rewrite default apples oranges cherries fruit_salad ([x] :: bowl)
23	+
24	+	rewrite defualt apples oranges cherries fruit_salad bowl =
25	+	[default, apples, oranges, cherries, fruit_salad, bowl]