Repository navigation
Expand file tree
/
Copy pathCases.lean
More file actions
67 lines (65 loc) · 2.11 KB
/
Copy pathCases.lean
File metadata and controls
67 lines (65 loc) · 2.11 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
import Examples.Scale.Cases
import TestSupport.Modules.Gcd
import Examples.SumArray.Cases
import Examples.PairSum.Cases
import Examples.SumCount.Cases
import Examples.Axpy.Cases
import Examples.ScaledHypot.Cases
import Examples.Binary32.Cases
import Examples.Piecewise.Cases
import TestSupport.Modules.SumSquares
import TestSupport.Modules.Mean
import Examples.Bucket.Cases
import Demos.Clob.Cases
import Examples.Calc.Cases
import Examples.Shape.Cases
import Examples.Lists.Cases
import Examples.Words.Cases
import Examples.Trees.Cases
import Examples.Updates.Cases
import Examples.Bools.Cases
import Examples.Grids.Cases
import Demos.Euler.Cases
import Demos.Drone.Cases
import Examples.Increment.Cases
import Examples.RemoveZero.Cases
import TestSupport.Modules.PrimeFactors
import Examples.Lookup.Cases
import Examples.Below100.Cases
import Examples.TreeLookup.Cases
/-! Test cases for the modules other than `gpt.wasm` and `prng.wasm`, computed by native
Lean. Each example's `Cases.lean` prints its cases, one line per case:
`module|export|result kind|host arguments|expected result`, with floats given as bit
patterns and a pair of arrays as the two arrays' words joined by a comma.
`tests/modules/run.sh` passes the arguments to the Wasmtime host running
`build/MODULE/MODULE.wasm` and compares its output. Run with `lake env lean --run`. -/
def main : IO Unit := do
Examples.Scale.cases
Library.Numerics.Arithmetic.Gcd.cases
Examples.SumArray.cases
Examples.PairSum.cases
Examples.SumCount.cases
Examples.Axpy.cases
Examples.ScaledHypot.cases
Examples.Binary32.cases
Examples.Piecewise.cases
Library.Numerics.Statistics.SumSquares.cases
Library.Numerics.Statistics.Mean.cases
Examples.Bucket.cases
Demos.Clob.cases
Examples.Calc.cases
Examples.Shape.cases
Examples.Lists.cases
Examples.Words.cases
Examples.Trees.cases
Examples.Updates.cases
Examples.Bools.cases
Examples.Grids.cases
Demos.Euler.cases
Demos.Drone.cases
Examples.Increment.cases
Examples.RemoveZero.cases
Library.Numerics.Arithmetic.PrimeFactors.cases
Examples.Lookup.cases
Examples.Below100.cases
Examples.TreeLookup.cases