From 051688f8fe0bd11773ebd5f0e762ff067e1fef8e Mon Sep 17 00:00:00 2001
From: "Emmanouil (Manos) Koukoutos" <emmanouil.koukoutos@epfl.ch>
Date: Mon, 6 Oct 2014 17:59:09 +0200
Subject: [PATCH] Option.get in Leon library
---
library/Option.scala | 8 ++++++++
1 file changed, 8 insertions(+)
diff --git a/library/Option.scala b/library/Option.scala
index e35fc9a0f..8769f3386 100644
--- a/library/Option.scala
+++ b/library/Option.scala
@@ -6,6 +6,14 @@ import leon.annotation._
@library
sealed abstract class Option[T] {
+
+ def get : T = {
+ require(this.isDefined)
+ this match {
+ case Some(x) => x
+ }
+ }
+
def getOrElse(default: T) = this match {
case Some(v) => v
case None() => default
--
GitLab