Ilya Yanok
23c9474092
[ whitespace ] untabify everything
|
%!s(int64=10) %!d(string=hai) anos | |
|---|---|---|
| .. | ||
| AlonzoPrelude.agda | %!s(int64=10) %!d(string=hai) anos | |
| BadPrintf.agda | %!s(int64=10) %!d(string=hai) anos | |
| BadPrintf2.agda | %!s(int64=10) %!d(string=hai) anos | |
| Bool.agda | %!s(int64=16) %!d(string=hai) anos | |
| Bool.hs | %!s(int64=10) %!d(string=hai) anos | |
| ListTest.agda | %!s(int64=16) %!d(string=hai) anos | |
| Makefile | %!s(int64=16) %!d(string=hai) anos | |
| Point.agda | %!s(int64=16) %!d(string=hai) anos | |
| Point.hs | %!s(int64=10) %!d(string=hai) anos | |
| PreludeAll.agda | %!s(int64=10) %!d(string=hai) anos | |
| PreludeBool.agda | %!s(int64=16) %!d(string=hai) anos | |
| PreludeInt.agda | %!s(int64=10) %!d(string=hai) anos | |
| PreludeList.agda | %!s(int64=10) %!d(string=hai) anos | |
| PreludeNat.agda | %!s(int64=16) %!d(string=hai) anos | |
| PreludeNatType.agda | %!s(int64=11) %!d(string=hai) anos | |
| PreludeNatType.hs | %!s(int64=10) %!d(string=hai) anos | |
| PreludeShow.agda | %!s(int64=10) %!d(string=hai) anos | |
| PreludeString.agda | %!s(int64=10) %!d(string=hai) anos | |
| Primitive.agda | %!s(int64=16) %!d(string=hai) anos | |
| PrintFloat.agda | %!s(int64=10) %!d(string=hai) anos | |
| PrintNat.agda | %!s(int64=10) %!d(string=hai) anos | |
| Printf.agda | %!s(int64=10) %!d(string=hai) anos | |
| Proj.agda | %!s(int64=10) %!d(string=hai) anos | |
| Q.agda | %!s(int64=10) %!d(string=hai) anos | |
| README | %!s(int64=16) %!d(string=hai) anos | |
| RTD.hs | %!s(int64=10) %!d(string=hai) anos | |
| RTN.agda | %!s(int64=11) %!d(string=hai) anos | |
| RTN.hs | %!s(int64=10) %!d(string=hai) anos | |
| RTP.agda | %!s(int64=10) %!d(string=hai) anos | |
| RTP.hs | %!s(int64=10) %!d(string=hai) anos | |
| RTP.hs.sav | %!s(int64=16) %!d(string=hai) anos | |
| RTS.hs | %!s(int64=10) %!d(string=hai) anos | |
| Records.agda | %!s(int64=16) %!d(string=hai) anos | |
| Records.hs | %!s(int64=10) %!d(string=hai) anos | |
| TestInt.agda | %!s(int64=10) %!d(string=hai) anos | |
| TestNat.agda | %!s(int64=16) %!d(string=hai) anos | |
| TestVec.agda | %!s(int64=10) %!d(string=hai) anos | |
| TestWith.agda | %!s(int64=10) %!d(string=hai) anos | |
| Vec.agda | %!s(int64=10) %!d(string=hai) anos | |
| almake | %!s(int64=16) %!d(string=hai) anos | |
README
== Using Alonzo ==
agda --alonzo File.agda
or
agda -c File.agda
produces File.hs
compile it with
ghc -c File.hs
The main module should contain the function mainS : String, compile it with
ghc --make -main-is File.main File.hs
There is a shell script "almake" that will do both, provided you have
compiled all dependencies beforehand.
Prerequisites
You need the following runtime files:
RTS.hs RTN.hs RTP.hs
RTN.agda RTP.agda
NEVER run agda -c on RT* files as it will destroy the corresponding .hs files
There is a "runtime" target in the Makefile, so running
make runtime
will compile the runtime files for you.
There is a small prelude included, you can compile it with
make prelude
agda --alonzo File.agda
or
agda -c File.agda
produces File.hs
compile it with
ghc -c File.hs
The main module should contain the function mainS : String, compile it with
ghc --make -main-is File.main File.hs
There is a shell script "almake" that will do both, provided you have
compiled all dependencies beforehand.
Prerequisites
You need the following runtime files:
RTS.hs RTN.hs RTP.hs
RTN.agda RTP.agda
NEVER run agda -c on RT* files as it will destroy the corresponding .hs files
There is a "runtime" target in the Makefile, so running
make runtime
will compile the runtime files for you.
There is a small prelude included, you can compile it with
make prelude