Initial commit
This commit is contained in:
commit
a5453cabbd
10 changed files with 71 additions and 0 deletions
3
.envrc
Normal file
3
.envrc
Normal file
|
@ -0,0 +1,3 @@
|
|||
source_env ../Idris
|
||||
|
||||
export RAKULIB=$PWD/lib
|
2
.gitignore
vendored
Normal file
2
.gitignore
vendored
Normal file
|
@ -0,0 +1,2 @@
|
|||
.env/
|
||||
.direnv/
|
2
Idris/.gitignore
vendored
Normal file
2
Idris/.gitignore
vendored
Normal file
|
@ -0,0 +1,2 @@
|
|||
build/
|
||||
*.*~
|
48
Idris/Idris.ipkg
Normal file
48
Idris/Idris.ipkg
Normal file
|
@ -0,0 +1,48 @@
|
|||
package Idris
|
||||
version = 0.1.0
|
||||
authors = "Nathan McCarty"
|
||||
-- maintainers =
|
||||
-- license =
|
||||
-- brief =
|
||||
-- readme =
|
||||
-- homepage =
|
||||
-- sourceloc =
|
||||
-- bugtracker =
|
||||
|
||||
-- the Idris2 version required (e.g. langversion >= 0.5.1)
|
||||
-- langversion
|
||||
|
||||
-- packages to add to search path
|
||||
-- depends =
|
||||
|
||||
-- modules to install
|
||||
modules = Idris
|
||||
, Posts.HelloWorld
|
||||
|
||||
-- main file (i.e. file to load at REPL)
|
||||
-- main =
|
||||
|
||||
-- name of executable
|
||||
-- executable =
|
||||
-- opts =
|
||||
sourcedir = "src"
|
||||
-- builddir =
|
||||
-- outputdir =
|
||||
|
||||
-- script to run before building
|
||||
-- prebuild =
|
||||
|
||||
-- script to run after building
|
||||
-- postbuild =
|
||||
|
||||
-- script to run after building, before installing
|
||||
-- preinstall =
|
||||
|
||||
-- script to run after installing
|
||||
-- postinstall =
|
||||
|
||||
-- script to run before cleaning
|
||||
-- preclean =
|
||||
|
||||
-- script to run after cleaning
|
||||
-- postclean =
|
4
Idris/pack.toml
Normal file
4
Idris/pack.toml
Normal file
|
@ -0,0 +1,4 @@
|
|||
[custom.all.Idris]
|
||||
type = "local"
|
||||
path = "."
|
||||
ipkg = "Idris.ipkg"
|
4
Idris/src/Idris.idr
Normal file
4
Idris/src/Idris.idr
Normal file
|
@ -0,0 +1,4 @@
|
|||
module Idris
|
||||
|
||||
test : String
|
||||
test = "Hello from Idris2!"
|
7
Idris/src/Posts/HelloWorld.md
Normal file
7
Idris/src/Posts/HelloWorld.md
Normal file
|
@ -0,0 +1,7 @@
|
|||
# Hello World
|
||||
|
||||
```idris
|
||||
module Posts.HelloWorld
|
||||
|
||||
%default total
|
||||
```
|
1
blog
Executable file
1
blog
Executable file
|
@ -0,0 +1 @@
|
|||
#!/usr/bin/env raku
|
0
db/.gitkeep
Normal file
0
db/.gitkeep
Normal file
0
lib/.gitkeep
Normal file
0
lib/.gitkeep
Normal file
Loading…
Add table
Reference in a new issue