intro

This repository implements indexed streams.

See here for the compiler and here for several example array kernels.

build proofs

First install lean3. In the root directory, run

leanproject get-mathlib-cache
leanproject build

build compiler

First install lean4. In the etch4 directory, run

lake build

then load Etch/Benchmark.lean in your editor.