Revision 25d7504145c07e4345a472338a8616b023fc8243 authored by Pierre-Yves Strub on 11 July 2015, 19:03:40 UTC, committed by Pierre-Yves Strub on 12 July 2015, 12:14:23 UTC
[fix #17219]
1 parent 9b8598c
Option.ec
(* --------------------------------------------------------------------
* Copyright (c) - 2012-2015 - IMDEA Software Institute and INRIA
* Distributed under the terms of the CeCILL-B licence.
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
op witness : 'a. (* All types are inhabited in EC *)
(* -------------------------------------------------------------------- *)
type 'a option = [None | Some of 'a].
op option_rect (v:'a) (f:'b -> 'a) xo =
with xo = None => v
with xo = Some x => f x.
op oapp ['a 'b] (f : 'a -> 'b) d ox : 'b =
with ox = None => d
with ox = Some x => f x.
op odflt (d : 'a) ox =
with ox = None => d
with ox = Some x => x.
op obind ['a 'b] (f : 'a -> 'b option) ox =
with ox = None => None
with ox = Some x => f x.
op omap ['a 'b] (f : 'a -> 'b) ox =
with ox = None => None
with ox = Some x => Some (f x).
op oget (ox : 'a option) = odflt witness<:'a> ox.
lemma nosmt oget_none: oget None<:'a> = witness.
proof. by []. qed.
lemma nosmt oget_some (x : 'a): oget (Some x) = x.
proof. by []. qed.
lemma nosmt someI (x y:'a): Some x = Some y => x = y by [].
lemma none_omap (f:'a -> 'b) ox:
omap f ox = None <=> ox = None
by case ox.
lemma oget_omap_some (f:'a -> 'b) ox:
ox <> None =>
oget (omap f ox) = f (oget ox)
by case ox.
Computing file changes ...