thatonelutenist/website
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Move idris projects to right place

Browse source
This commit is contained in:
Nathan McCarty 2025-01-20 21:54:54 -05:00
parent edf363e442
commit 43585ac89e
5 changed files with 0 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

4
projects/Idris/src/Idris.idr Normal file
View file

@ -0,0 +1,4 @@
module Idris
test : String
test = "Hello from Idris2!"

7
projects/Idris/src/Posts/HelloWorld.md Normal file
View file

@ -0,0 +1,7 @@
# Hello World
```idris
module Posts.HelloWorld
%default total
```