diff options
author | 2013-11-02 15:41:37 +0000 | |
---|---|---|
committer | 2013-11-02 15:41:37 +0000 | |
commit | 7a7c00fdc81b450a5b2cb91b64bb2602d24212c1 (patch) | |
tree | a87e0dc7e939b3b5b0536177fe50c38ddcb169d1 /bootstrap/Monads.v | |
parent | 1a8def9dc4380b221b5b457f06b12e0a73a3811a (diff) |
Cleanup of comments in bootstrap/Monads.v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17031 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'bootstrap/Monads.v')
-rw-r--r-- | bootstrap/Monads.v | 25 |
1 files changed, 3 insertions, 22 deletions
diff --git a/bootstrap/Monads.v b/bootstrap/Monads.v index a6b7bad12..6cf0b1396 100644 --- a/bootstrap/Monads.v +++ b/bootstrap/Monads.v @@ -288,9 +288,9 @@ Module IO. End IO. Module State. -(** The impredicative encoding of the usual State predicate - transformer (StateT in Haskell). The impredicative encoding allows - to avoid creating blocks (val,state) at each bind. *) +(** The impredicative encoding of the usual State monad transformer + (StateT in Haskell). The impredicative encoding allows to avoid + creating blocks (val,state) at each bind. *) Section Common. @@ -476,12 +476,6 @@ Module Logic. result, sequentialising with a [f:'a -> 'b t] is done by applying [f] to each element and then flatten the list, [plus] is concatenation, and [split] is pattern-matching. *) -(* spiwack: I added the primitives from [IO] directly in the [Logic] - signature for convenience. It doesn't really make sense, strictly - speaking, as they are somewhat deconnected from the semantics of - [Logic], but without an appropriate language for composition (some - kind of mixins?) I would be going nowhere with a gazillion - functors. *) Section Common. @@ -685,19 +679,6 @@ Module Logical. Definition split {a:Set} (x:t a) : t (list_view a (Exception -> t a)) := Eval compute in freeze _ (split0 x). -(* - Eval compute in - freeze _ ( - do NonLogicalMonad r := - Logic.reify (Writer.reify (Environment.reify (State.reify x))) - in - match r with - | inr e => _zero e - | inl (a,x) => _plus (ret _ F a) x - ). - -split _ LogicalLogic x). -*) Extraction Implicit split [a]. Definition lift {a:Set} (x:NonLogical.t a) : t a := Eval compute in freeze _ (State.lift _ _ LogicalMonadEnv (Environment.lift _ _ LogicalMonadWriter (Writer.lift _ LogicalMessage _ LogicalMonadBase (Logic.lift _ NonLogicalMonad x)))). |