File: RunIO.v

package info (click to toggle)
coq-simple-io 1.11.0-1
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid, trixie
  • size: 380 kB
  • sloc: ml: 273; makefile: 66
file content (18 lines) | stat: -rw-r--r-- 400 bytes parent folder | download 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
 
From Coq Require Import
     ExtrOcamlIntConv
     String.
From ExtLib Require Import
     Monad.
From SimpleIO Require Import
     IO_Random
     SimpleIO.
Import
  MonadNotation.
Open Scope monad_scope.
Open Scope string_scope.

Definition coin : IO unit :=
  b <- ORandom.bool tt;;
  print_endline (if b : bool then "head" else "tail").

RunIO (ORandom.init (int_of_nat 42);; coin;; coin;; coin).