https://github.com/EasyCrypt/easycrypt
Revision 3fb5602c88dbf5e78575762c9b668fa6733d7298 authored by Pierre-Yves Strub on 05 July 2014, 12:20:08 UTC, committed by Pierre-Yves Strub on 05 July 2014, 12:20:08 UTC
1 parent a7bea72
Tip revision: 3fb5602c88dbf5e78575762c9b668fa6733d7298 authored by Pierre-Yves Strub on 05 July 2014, 12:20:08 UTC
[rewrite smt]: call [smt].
[rewrite smt]: call [smt].
Tip revision: 3fb5602
Option.ec
(* --------------------------------------------------------------------
* Copyright IMDEA Software Institute / INRIA - 2013, 2014
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
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 ...