-
Notifications
You must be signed in to change notification settings - Fork 2
Open
Description
Это баг или фича?
let rec append xs ys =
match xs with
| [] -> ys
| h :: tl -> h :: append tl ys
;;
let my_remove : 'a -> 'a list -> 'a list option =
fun item xs ->
let rec helper acc xs =
match xs with
| [] -> None
| h :: tl -> if h = item then Some (append acc tl) else helper (h :: acc) tl
in
helper [] xs
;;Генеренный код орёт
File "lozovml/attempt_common.ml", lines 12-18, characters 4-30:
12 | ....fun xs ->
13 | fun q37 ->
14 | let rec helper acc xs q28 =
15 | ((xs === (nil ())) &&& (q28 === (none ()))) |||
16 | (fresh (h tl q31) (xs === (h % tl)) (conde [(h === item) &&& (q31 === (!! true)); (q31 === (!! false)) &&& (h =/= item)])
17 | (conde [fresh (q32) (q31 === (!! true)) (q28 === (some q32)) (append acc tl q32); (q31 === (!! false)) &&& (helper (h % acc) tl q28)])) in
18 | helper (nil ()) xs q37
Error: This function expects too many arguments, it should have type
'a -> 'a GT.list -> 'a GT.list GT.option
Metadata
Metadata
Assignees
Labels
No labels