Ilya Yanok
23c9474092
[ whitespace ] untabify everything
|
vor 10 Jahren | |
|---|---|---|
| .. | ||
| AlonzoPrelude.agda | vor 10 Jahren | |
| BadPrintf.agda | vor 10 Jahren | |
| BadPrintf2.agda | vor 10 Jahren | |
| Bool.agda | vor 16 Jahren | |
| Bool.hs | vor 10 Jahren | |
| ListTest.agda | vor 16 Jahren | |
| Makefile | vor 16 Jahren | |
| Point.agda | vor 16 Jahren | |
| Point.hs | vor 10 Jahren | |
| PreludeAll.agda | vor 10 Jahren | |
| PreludeBool.agda | vor 16 Jahren | |
| PreludeInt.agda | vor 10 Jahren | |
| PreludeList.agda | vor 10 Jahren | |
| PreludeNat.agda | vor 16 Jahren | |
| PreludeNatType.agda | vor 11 Jahren | |
| PreludeNatType.hs | vor 10 Jahren | |
| PreludeShow.agda | vor 10 Jahren | |
| PreludeString.agda | vor 10 Jahren | |
| Primitive.agda | vor 16 Jahren | |
| PrintFloat.agda | vor 10 Jahren | |
| PrintNat.agda | vor 10 Jahren | |
| Printf.agda | vor 10 Jahren | |
| Proj.agda | vor 10 Jahren | |
| Q.agda | vor 10 Jahren | |
| README | vor 16 Jahren | |
| RTD.hs | vor 10 Jahren | |
| RTN.agda | vor 11 Jahren | |
| RTN.hs | vor 10 Jahren | |
| RTP.agda | vor 10 Jahren | |
| RTP.hs | vor 10 Jahren | |
| RTP.hs.sav | vor 16 Jahren | |
| RTS.hs | vor 10 Jahren | |
| Records.agda | vor 16 Jahren | |
| Records.hs | vor 10 Jahren | |
| TestInt.agda | vor 10 Jahren | |
| TestNat.agda | vor 16 Jahren | |
| TestVec.agda | vor 10 Jahren | |
| TestWith.agda | vor 10 Jahren | |
| Vec.agda | vor 10 Jahren | |
| almake | vor 16 Jahren | |
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