-
David Swasey authored
The old fill_value K e : is_value (fill K e) -> K = empty_ctx. won't work. Counterexamples: K=(v,•) or K=inl • satisfy is_value K[v] for reasonable choices of is_value.
1ebc9a44
The old fill_value K e : is_value (fill K e) -> K = empty_ctx. won't work. Counterexamples: K=(v,•) or K=inl • satisfy is_value K[v] for reasonable choices of is_value.