Idris-dev/test/reg005/run

mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-11-15 01:25:05 +03:00
#!/bin/bash
idris $@ reg005.idr -o reg005
./reg005
rm -f reg005 *.ibc
Normalise LHS before compilation ...otherwise in some situations the forcing optimisation may lead to uncompilable code 2012-11-21 20:32:18 +04:00			`#!/bin/bash`
			`idris $@ reg005.idr -o reg005`
			`./reg005`
			`rm -f reg005 *.ibc`