capitalex ревизій цього gist . До ревизії
1 file changed, 0 insertions, 0 deletions
rewrite.idris перейменовано в rewrite.idr
Файл перейменовано без змін
capitalex ревизій цього gist . До ревизії
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] | |
Новіше
Пізніше