mirror of
https://github.com/anoma/juvix.git
synced 2024-12-15 01:52:11 +03:00
63 lines
1.1 KiB
Plaintext
63 lines
1.1 KiB
Plaintext
module Input;
|
||
|
||
builtin bool
|
||
inductive Bool {
|
||
true : Bool;
|
||
false : Bool;
|
||
};
|
||
|
||
builtin bool-if
|
||
if : {A : Type} → Bool → A → A → A;
|
||
if true t _ := t;
|
||
if false _ e := e;
|
||
|
||
builtin nat
|
||
inductive ℕ {
|
||
zero : ℕ;
|
||
suc : ℕ → ℕ;
|
||
};
|
||
|
||
boolToNat : Bool → ℕ;
|
||
boolToNat false := zero;
|
||
boolToNat true := suc zero;
|
||
|
||
infixl 4 +;
|
||
builtin nat-plus
|
||
+ : ℕ → ℕ → ℕ;
|
||
+ zero x := x;
|
||
+ (suc a) b := suc (a + b);
|
||
|
||
mult : ℕ → ℕ → ℕ;
|
||
mult zero _ := zero;
|
||
mult (suc n) m := m + (mult n m);
|
||
|
||
plusOne : ℕ → ℕ;
|
||
plusOne := suc;
|
||
|
||
someLiteral : _;
|
||
someLiteral := 123;
|
||
|
||
infix 4 ==;
|
||
== : ℕ → ℕ → Bool;
|
||
== zero zero := true;
|
||
== (suc n) (suc m) := n == m;
|
||
== _ _ := false;
|
||
|
||
builtin IO axiom IO : Type;
|
||
|
||
infixl 1 >>;
|
||
builtin IO-sequence axiom >> : IO → IO → IO;
|
||
builtin nat-print axiom printNat : ℕ → IO;
|
||
|
||
main : IO;
|
||
main := printNat (boolToNat true)
|
||
>> printNat (boolToNat false)
|
||
>> printNat (mult 3 (2 + 2))
|
||
>> printNat 2
|
||
>> printNat (if (1 == 2) 100 200)
|
||
>> printNat (if (1 == 1) 300 400)
|
||
>> if (1 == 2) (printNat 500) (printNat 600)
|
||
>> if (1 == 1) (printNat 700) (printNat 800);
|
||
|
||
end;
|