fabian/veribase-idr2 - Change NYMIFK2WBHU4G34QF4GZP63ATL2EQC6PLAQLWZMUTPDGDPQUEKVQC

Make a HelloWorld sample work

Created by fabian on June 7, 2021

NYMIFK2WBHU4G34QF4GZP63ATL2EQC6PLAQLWZMUTPDGDPQUEKVQC

Dependencies

In channels

main

Change contents

Replacement in src/PrimIO.idr at line 39 [4.75]
B:BD[4.1699] → [4.1699:1721]
```
import public Builtin
```
[4.1699]
[4.1721]
```
import Builtin
```
Replacement in src/PrimIO.idr at line 43 [4.75]
B:BD[4.1738] → [4.1738:1752]
```
public export
```
[4.1738]
[4.1752]
```
export
```

Insertion in src/PrimIO.idr at line 58 [4.75]

[4.2079]


unsafeCreateWorld : (%World -> a) -> a
unsafeCreateWorld f = f %MkWorld
unsafeDestroyWorld : %World -> a -> a
unsafeDestroyWorld %MkWorld x = x
public export
data IO : Type -> Type where
  MkIO : PrimIO a -> IO a
public export
unsafePerformIO : IO a -> a
unsafePerformIO (MkIO p) = unsafeCreateWorld (\w =>
  let MkIORes res w' := p w in unsafeDestroyWorld w' res)

Replacement in src/Data/Optional.idr at line 81 [6.30]

B:BD[5.58] → [5.58:110]

  bind Nothing  _ = Nothing
  bind (Some x) f = f x

[5.58]

[5.110]

  Nothing >>= _ = Nothing
  (Some x) >>= f = f x

Insertion in src/Data/LinkedList.idr at line 4 [7.17]
[7.57]
[7.57]
```
import Algebra.Relation.Equivalence
```
Deletion in src/Data/LinkedList.idr at line 8 [7.17]
B:BD[8.787] → [8.787:823]
```
import Algebra.Relation.Equivalence
```
Insertion in src/Data/LinkedList.idr at line 10 [7.17]
[8.883]
[8.883]
```
import Algebra.Group.Magma
```
Insertion in src/Data/LinkedList.idr at line 13 [7.17]
[8.911]
[7.108]
```
import Algebra.Group.Semigroup
```

Replacement in src/Data/LinkedList.idr at line 143 [7.17]

B:BD[9.212] → [9.212:271]

  bind Nil _ = Nil
  bind (x::xs) f = f x <> (xs `bind` f)

[9.212]

[9.271]

  Nil >>= _ = Nil
  (x::xs) >>= f = f x <> (xs >>= f)

Replacement in src/Data/Either.idr at line 3 [10.13]
B:BD[10.34] → [10.34:56]
```
import public Builtin
```
[10.34]
[10.56]
```
import Builtin
```

Replacement in src/Data/Either.idr at line 50 [10.13]

B:BD[10.1045] → [10.1045:1102]

  (Left x)  `bind` _ = Left x
  (Right x) `bind` f = f x

[10.1045]

[10.1102]

  (Left x)  >>= _ = Left x
  (Right x) >>= f = f x

Replacement in src/Data/Boolean.idr at line 3 [6.117]
B:BD[6.139] → [11.0:22]
```
import public Builtin
```
[6.139]
[12.207]
```
import Builtin
```

Replacement in src/Data/Boolean.idr at line 5 [6.117]

B:BD[12.208] → [8.577:620]

B:BD[8.620] → [13.113:190]

import public Algebra.Relation.Equivalence
import public Algebra.Relation.Preorder
import public Algebra.Relation.Order

[12.208]

[2.138]

import Algebra.Relation.Equivalence
import Algebra.Relation.Preorder
import Algebra.Relation.Order

Replacement in src/Data/Boolean.idr at line 9 [6.117]
∅:D[2.139] → [8.620:655]
∅:D[13.190] → [8.620:655]
B:BD[8.620] → [8.620:655]
```
import public Algebra.Group.Monoid
```
[2.139]
[2.140]
```
import Algebra.Group.Magma
import Algebra.Group.Monoid
import Algebra.Group.Semigroup
```

Replacement in src/Data/Boolean.idr at line 13 [6.117]

B:BD[2.141] → [2.141:233]

import public Algebra.Lattice.JoinSemilattice
import public Algebra.Lattice.MeetSemilattice

[2.141]

[13.191]

import Algebra.Lattice.JoinSemilattice
import Algebra.Lattice.MeetSemilattice

Replacement in src/Control/IO.idr at line 3 [4.2100]
B:BD[4.2120] → [4.2120:2141]
```
import public PrimIO
```
[4.2120]
[4.2141]
```
import Builtin
import PrimIO
```
Deletion in src/Control/IO.idr at line 15 [4.2100]
B:BD[4.2292] → [4.2292:2362]
```
data IO : Type -> Type where
  MkIO : PrimIO a -> IO a
public export
```
Replacement in src/Control/IO.idr at line 36 [4.2100]
B:BD[4.2883] → [4.2883:2911]
```
  bind (MkIO px) f = MkIO (
```
[4.2883]
[4.2911]
```
  (MkIO px) >>= f = MkIO (
```
Insertion in src/Control/Console.idr at line 2 [4.3613]
[4.3637]
[4.3637]
```
import Builtin
```
Replacement in src/Control/Console.idr at line 5 [4.3613]
B:BD[4.3638] → [4.3638:3660]
```
import public Builtin
```
[4.3638]
[4.3660]
```
import Algebra.Control.Monad
```
Replacement in src/Control/Console.idr at line 10 [4.3613]
B:BD[4.3691] → [4.3691:3717]
```
interface Console t where
```
[4.3691]
[4.3717]
```
interface Monad t => Console t where
```
Replacement in src/Algebra/Relation/Preorder.idr at line 3 [14.531]
B:BD[14.566] → [14.566:588]
```
import public Builtin
```
[14.566]
[14.588]
```
import Builtin
```
Replacement in src/Algebra/Relation/Order.idr at line 3 [14.12]
B:BD[14.44] → [14.44:66]
```
import public Builtin
```
[14.44]
[14.66]
```
import Builtin
```

Replacement in src/Algebra/Relation/Order.idr at line 5 [14.12]

B:BD[14.67] → [14.67:150]

import public Algebra.Relation.Preorder
import public Algebra.Relation.Equivalence

[14.67]

[14.150]

import Algebra.Relation.Preorder
import Algebra.Relation.Equivalence

Replacement in src/Algebra/Relation/Order.idr at line 8 [14.12]
B:BD[14.151] → [13.0:26]
```
import public Data.Either
```
[14.151]
[3.17]
```
import Data.Either
```
Replacement in src/Algebra/Lattice/MeetSemilattice.idr at line 3 [15.581]
B:BD[15.622] → [15.622:644]
```
import public Builtin
```
[15.622]
[15.644]
```
import Builtin
```
Replacement in src/Algebra/Lattice/MeetSemilattice.idr at line 5 [15.581]
B:BD[15.645] → [15.645:682]
```
import public Algebra.Relation.Order
```
[15.645]
[15.682]
```
import Algebra.Relation.Preorder
import Algebra.Relation.Order
```
Replacement in src/Algebra/Lattice/JoinSemilattice.idr at line 3 [15.33]
B:BD[15.74] → [15.74:96]
```
import public Builtin
```
[15.74]
[15.96]
```
import Builtin
```
Replacement in src/Algebra/Lattice/JoinSemilattice.idr at line 5 [15.33]
B:BD[15.97] → [15.97:134]
```
import public Algebra.Relation.Order
```
[15.97]
[15.134]
```
import Algebra.Relation.Preorder
import Algebra.Relation.Order
```
Replacement in src/Algebra/Group/Semigroup.idr at line 5 [16.639]
B:BD[16.682] → [8.475:509]
```
import public Algebra.Group.Magma
```
[16.682]
[3.34]
```
import Algebra.Group.Magma
```
Replacement in src/Algebra/Group/Monoid.idr at line 5 [16.395]
B:BD[16.435] → [8.388:426]
```
import public Algebra.Group.Semigroup
```
[16.435]
[3.51]
```
import Algebra.Group.Magma
import Algebra.Group.Semigroup
```

Replacement in src/Algebra/Group/Group.idr at line 5 [16.12]

B:BD[16.51] → [8.270:305]

import public Algebra.Group.Monoid

[16.51]

[3.85]

import Algebra.Group.Magma
import Algebra.Group.Monoid
import Algebra.Group.Semigroup

Insertion in src/Algebra/Control/Monad.idr at line 8 [17.12]
[17.94]
[17.94]
```
infixl 1 >>=, >>
```
Replacement in src/Algebra/Control/Monad.idr at line 13 [17.12]
B:BD[17.150] → [17.150:184]
```
  bind : t a -> (a -> t b) -> t b
```
[17.150]
[17.184]
```
  (>>=) : t a -> (a -> t b) -> t b
```

Replacement in src/Algebra/Control/Monad.idr at line 15 [17.12]

B:BD[17.185] → [17.185:336]

  proofLeftIdentity : (x : a) -> (f : a -> t b) -> Applicative.pure x `bind` f = f x
  proofRightIdentity : (x : t a) -> x `bind` Applicative.pure = x

[17.185]

[17.336]

  proofLeftIdentity : (x : a) -> (f : a -> t b) -> Applicative.pure x >>= f = f x
  proofRightIdentity : (x : t a) -> x >>= Applicative.pure = x

Replacement in src/Algebra/Control/Monad.idr at line 18 [17.12]

B:BD[17.405] → [17.405:483]

                     -> (x `bind` f) `bind` g = x `bind` (\x => f x `bind` g)

[17.405]

                     -> (x >>= f) >>= g = x >>= (\x => f x >>= g)
public export
(>>) : Monad t => t a -> t b -> t b
mx >> my = (mx >>= (\_ => my))

File addition: samples (d--x------)
[1.0]

File addition: HelloWorld.idr (----------)

[0.1908]

import Builtin
import PrimIO
import Algebra.Control.Monad
import Control.Console
import Control.IO
askName : Console m => m ()
askName = do
  putLine "What's your name? "
  name <- getLine
  putString "Hello, "
  putString name
  putChar '!'
  putChar '\n'
main : IO ()
main = askName

Make a HelloWorld sample work

Dependencies

In channels

Change contents

Replacement in src/PrimIO.idr at line 39 [4.75]

Replacement in src/PrimIO.idr at line 43 [4.75]

Insertion in src/PrimIO.idr at line 58 [4.75]

Replacement in src/Data/Optional.idr at line 81 [6.30]

Insertion in src/Data/LinkedList.idr at line 4 [7.17]

Deletion in src/Data/LinkedList.idr at line 8 [7.17]

Insertion in src/Data/LinkedList.idr at line 10 [7.17]

Insertion in src/Data/LinkedList.idr at line 13 [7.17]

Replacement in src/Data/LinkedList.idr at line 143 [7.17]

Replacement in src/Data/Either.idr at line 3 [10.13]

Replacement in src/Data/Either.idr at line 50 [10.13]

Replacement in src/Data/Boolean.idr at line 3 [6.117]

Replacement in src/Data/Boolean.idr at line 5 [6.117]

Replacement in src/Data/Boolean.idr at line 9 [6.117]

Replacement in src/Data/Boolean.idr at line 13 [6.117]

Replacement in src/Control/IO.idr at line 3 [4.2100]

Deletion in src/Control/IO.idr at line 15 [4.2100]

Replacement in src/Control/IO.idr at line 36 [4.2100]

Insertion in src/Control/Console.idr at line 2 [4.3613]

Replacement in src/Control/Console.idr at line 5 [4.3613]

Replacement in src/Control/Console.idr at line 10 [4.3613]

Replacement in src/Algebra/Relation/Preorder.idr at line 3 [14.531]

Replacement in src/Algebra/Relation/Order.idr at line 3 [14.12]

Replacement in src/Algebra/Relation/Order.idr at line 5 [14.12]

Replacement in src/Algebra/Relation/Order.idr at line 8 [14.12]

Replacement in src/Algebra/Lattice/MeetSemilattice.idr at line 3 [15.581]

Replacement in src/Algebra/Lattice/MeetSemilattice.idr at line 5 [15.581]

Replacement in src/Algebra/Lattice/JoinSemilattice.idr at line 3 [15.33]

Replacement in src/Algebra/Lattice/JoinSemilattice.idr at line 5 [15.33]

Replacement in src/Algebra/Group/Semigroup.idr at line 5 [16.639]

Replacement in src/Algebra/Group/Monoid.idr at line 5 [16.395]

Replacement in src/Algebra/Group/Group.idr at line 5 [16.12]

Insertion in src/Algebra/Control/Monad.idr at line 8 [17.12]

Replacement in src/Algebra/Control/Monad.idr at line 13 [17.12]

Replacement in src/Algebra/Control/Monad.idr at line 15 [17.12]

Replacement in src/Algebra/Control/Monad.idr at line 18 [17.12]

File addition: samples (d--x------)

File addition: HelloWorld.idr (----------)