Fix comment (#103)

By submitting this pull request, I confirm that my contribution is made
under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).

audit.log

@@ -1,6 +1,6 @@
 src/Distributions/BernoulliExpNeg/Correctness.dfy(13,17): Correctness: Declaration has explicit `{:axiom}` attribute. 
 src/Distributions/BernoulliExpNeg/Correctness.dfy(17,17): SampleIsIndep: Declaration has explicit `{:axiom}` attribute. 
-src/Distributions/BernoulliExpNeg/Model.dfy(100,17): GammaLe1LoopTerminatesAlmostSurely: Declaration has explicit `{:axiom}` attribute. 
+src/Distributions/BernoulliExpNeg/Model.dfy(104,17): GammaLe1LoopTerminatesAlmostSurely: Declaration has explicit `{:axiom}` attribute. 
 src/Distributions/Coin/Interface.dfy(21,6): CoinSample: Definition has `assume {:axiom}` statement in body. 
 src/Distributions/Uniform/Implementation.dfy(46,6): UniformSample: Definition has `assume {:axiom}` statement in body. 
 src/Math/Analysis/Reals.dfy(35,17): LeastUpperBoundProperty: Declaration has explicit `{:axiom}` attribute. 

src/Distributions/BernoulliExpNeg/Model.dfy

@@ -21,10 +21,12 @@ module BernoulliExpNeg.Model {
       (bgamma: (bool, Rationals.Rational)) =>
         var res: Monad.Hurd<bool> :=
           if bgamma.0 then
-            // This if condition should not be needed, but Monad.Bind does not accept functions with preconditions
+            // The else path should never be taken, but we cannot turn this into a precondition
+            // because Monad.Bind does not accept functions with preconditions.
+            // We return a dummy value in the else-branch.
             if 0 <= bgamma.1.numer <= bgamma.1.denom
             then SampleGammaLe1(bgamma.1)
-            else Monad.Return(false) // return a dummy value because this path should never be taken
+            else Monad.Return(false) // dummy value
           else
             Monad.Return(false);
         res
@@ -41,10 +43,12 @@ module BernoulliExpNeg.Model {
         GammaReductionLoopIter(bgamma),
         (bgamma': (bool, Rationals.Rational)) =>
           var res: Monad.Hurd<(bool, Rationals.Rational)> :=
-            // This if condition should not be needed, but Monad.Bind does not accept functions with preconditions
-            if bgamma'.1.numer < 0 || bgamma'.1.numer >= bgamma.1.numer
-            then Monad.Return((bgamma'.0, Rationals.Rational(0, 1)))
-            else GammaReductionLoop(bgamma'); // return a dummy value because this path should never be taken
+            // The else path should never be taken, but we cannot turn this into a precondition
+            // because Monad.Bind does not accept functions with preconditions.
+            // We return a dummy value in the else-branch.
+            if 0 <= bgamma'.1.numer < bgamma.1.numer
+            then GammaReductionLoop(bgamma')
+            else Monad.Return((bgamma'.0, Rationals.Rational(0, 1))); // dummy value
           res
       )
   }