#!/bin/bash
idris test002.idr --check --noprelude