mirror of
https://github.com/anoma/juvix.git
synced 2024-12-15 01:52:11 +03:00
27 lines
283 B
Plaintext
27 lines
283 B
Plaintext
|
module Input;
|
||
|
|
||
|
inductive Unit {
|
||
|
unit : Unit;
|
||
|
};
|
||
|
|
||
|
terminating
|
||
|
loop : {A : Type} -> A;
|
||
|
loop := loop;
|
||
|
|
||
|
const : {A : Type} -> A -> A -> A;
|
||
|
const x y := x;
|
||
|
|
||
|
fail : Unit;
|
||
|
fail := const unit loop;
|
||
|
|
||
|
axiom Action : Type;
|
||
|
|
||
|
compile Action {
|
||
|
c ↦ "int";
|
||
|
};
|
||
|
|
||
|
main : Action;
|
||
|
main := 0;
|
||
|
|
||
|
end;
|