famubu
/
playground
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

[twelf] start a hello-world kind of file

This commit is contained in:
Julin S 2024-04-07 18:33:16 +05:30
parent 118b3a9fe4
commit 4380c7c126
2 changed files with 25 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

24
twelf/hello/hello.elf Normal file
View File

@ -0,0 +1,24 @@
nat: type.
z: nat.
s: nat -> nat.
%name nat N.
evenOnly: nat -> type.
evenOnly/z: evenOnly z.
evenOnly/s: evenOnly (s (s N)) <- evenOnly N.
even: nat -> type.
odd: nat -> type.
even/z: even z.
even/s: even (s N) <- odd N.
odd/n: odd (s N) <- even N.
%%
evenOnly-implies-even: evenOnly N -> even N -> type.
%mode evenOnly-implies-even +X1 -X2.
evenOnly-implies-even/z: evenOnly-implies-even evenOnly/z even/z.
% evenOnly-implies-even/s: evenOnly-implies-even (evenOnly/s (s (s N))) (even/s (s (s N))).

1
twelf/hello/sources.cfg Normal file
View File

@ -0,0 +1 @@
hello.elf