Commit 531d88c1 authored by Ralf Jung's avatar Ralf Jung

give the fold_left version of fill

parent 4aeb0a86
......@@ -136,7 +136,9 @@ Definition ectx_item_fill (Ki : ectx_item) (e : expr) : expr :=
end.
Fixpoint fill K e :=
(* FIXME RJ: This really is fold_left, but if I use that all automation breaks. *)
(* FIXME RJ: This really is fold_left, but if I use that all automation breaks:
fold_left (fun e Ki => ectx_item_fill Ki e).
Or maybe we even have a combinator somewhere to swap the arguments? *)
match K with [] => e | Ki :: K => ectx_item_fill Ki (fill K e) end.
(** The stepping relation *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment