GitHub - dvlasits/Low-Level-Programming-with-Dependent-Types

Please find simple examples of the library in action in the examples.idr:

There you can see all the functions called e_ give a type error for some kind of unsafe behaviour with arrays.

The code which is executed by C is in the smallc.c file

I am now developing polymorphic Arrays + Structs in the linearLibPoly2.idr file

Name		Name	Last commit message	Last commit date
Latest commit History 41 Commits
.gitignore		.gitignore
BinarySearch.idr		BinarySearch.idr
Lib1.idr		Lib1.idr
LinearLibPoly6.idr		LinearLibPoly6.idr
LinearLibPoly7.idr		LinearLibPoly7.idr
LinearLibPoly8.idr		LinearLibPoly8.idr
LinearLibPoly9.idr		LinearLibPoly9.idr
Low-Level Programming with Dependent Types.pdf		Low-Level Programming with Dependent Types.pdf
README.md		README.md
UsingPolyLib.idr		UsingPolyLib.idr
arrayWrite.c		arrayWrite.c
binarySearchFinal.idr		binarySearchFinal.idr
datatest.idr		datatest.idr
examples.idr		examples.idr
helpful.idr		helpful.idr
helpfulLinear.idr		helpfulLinear.idr
helpfulLinearPoly.idr		helpfulLinearPoly.idr
linearLib.idr		linearLib.idr
linearLibPoly.idr		linearLibPoly.idr
linearLibPoly2.idr		linearLibPoly2.idr
linearTry.idr		linearTry.idr
lowlevel.idr		lowlevel.idr
makefile		makefile
pointer_functions.c		pointer_functions.c
pythonProfile.py		pythonProfile.py
pythonProfile2.py		pythonProfile2.py
smallc.c		smallc.c
test.idr		test.idr
testingBin.idr		testingBin.idr

Provide feedback