chore: move tests to new frontend

This commit is contained in:
Leonardo de Moura 2020-10-23 16:18:52 -07:00
parent 78c05e8f46
commit 21587ff19b
5 changed files with 21 additions and 15 deletions

View file

@ -1,5 +1,6 @@
def check (b : Bool) : IO Unit :=
unless b $ IO.println "failed"
#lang lean4
def check (b : Bool) : IO Unit := do
unless b do IO.println "failed"
def main : IO Unit :=

View file

@ -1,3 +1,5 @@
#lang lean4
def main : IO Unit :=
IO.println (strictOr false false) *>
IO.println (strictOr false true) *>

View file

@ -1,3 +1,4 @@
#lang lean4
def main (xs : List String) : IO UInt32 :=
IO.println "hello world" *>
pure 0

View file

@ -1,27 +1,28 @@
#eval do
t1 ← IO.asTask $ Nat.forM 10 fun _ => IO.println "hi";
t2 ← IO.asTask $ Nat.forM 10 fun _ => IO.println "ho";
#lang lean4
#eval id (α := IO _) do
let t1 ← IO.asTask $ Nat.forM 10 fun _ => IO.println "hi";
let t2 ← IO.asTask $ Nat.forM 10 fun _ => IO.println "ho";
IO.ofExcept t1.get
#eval do
t1 ← IO.mapTask IO.println (Task.spawn fun _ => "ha");
#eval id (α := IO _) do
let t1 ← IO.mapTask IO.println (Task.spawn fun _ => "ha");
pure ()
#eval do
t1 ← IO.bindTask (Task.spawn fun _ => "hu") fun s =>
#eval id (α := IO _) do
let t1 ← IO.bindTask (Task.spawn fun _ => "hu") fun s =>
IO.asTask (IO.println s);
pure ()
#eval do
t1 ← IO.asTask do {
c ← IO.checkCanceled;
#eval id (α := IO _) do
let t1 ← IO.asTask do {
let c ← IO.checkCanceled;
IO.println (if c then "canceled!" else "done!")
};
pure ()
#eval do
t1 ← IO.asTask do {
c ← IO.checkCanceled;
#eval id (α := IO _) do
let t1 ← IO.asTask do {
let c ← IO.checkCanceled;
IO.println (if c then "canceled! 2" else "done! 2")
};
IO.cancel t1;

View file

@ -1,3 +1,4 @@
#lang lean4
import Lean.Expr
open Lean