Open aryairani opened 2 years ago
and here's that definition, for reference:
fundamentals.abilities.exercises.ex1 : Doc
fundamentals.abilities.exercises.ex1 =
use Map get
{{
{{ exercise }} Exercise: Implement functions with calls to Ability operations
Given the type signatures below, implement the functions to satisfy the
compiler using the request operations of the Ability or functions found in
''.base''
@typecheck ```
getWithAbort : a -> Map a b ->{Abort} b
getWithAbort key map = todo "implement me!"
{{ Folded true {{ {{ hint }} Hint: how do I see the request operations of an ability? }} {{ In the UCM, you can enter ''view Abort'' to see the ability definition. The function signatures after the ''where'' keyword are the request operations. }} }}
{{ Folded true {{ {{ answer }} Answer: }} {{ Using the {toAbort} function.
@typecheck ```
let
getWithAbort : a -> Map a b ->{Abort} b
getWithAbort key map = toAbort (get key map)
```
Pattern matching on {type Optional}
@typecheck ```
let
getWithAbort : a -> Map a b ->{Abort} b
getWithAbort key map =
match get key map with
Some a -> a
None -> abort
``` }} }}
}}
Hopefully will fix these definitions from the repo in the description:
Here's a transcript to reproduce