mirror of
https://github.com/anoma/juvix.git
synced 2024-12-03 09:41:10 +03:00
83539148cb
* Closes #3079 * Closes #3086 * Depends on #3088 * Updates the coding style guidelines (CODING.md) to reflect issues not foreseen originally * Changes the unicode arrow printed in the REPL to `->`. This is to make the output consistent with how function types are written in the standard library. --------- Co-authored-by: Paul Cadman <git@paulcadman.dev>
34 lines
799 B
Plaintext
34 lines
799 B
Plaintext
-- Default values inserted in the arity checker
|
|
module test069;
|
|
|
|
import Stdlib.Data.Nat open hiding {Ord; mkOrd};
|
|
import Stdlib.Data.Nat.Ord as Ord;
|
|
import Stdlib.Data.Pair as Ord;
|
|
import Stdlib.Data.Bool.Base open;
|
|
import Stdlib.Trait.Ord open using {Ordering; LessThan; Equal; GreaterThan; isLessThan; isGreaterThan};
|
|
|
|
trait
|
|
type Ord A :=
|
|
mkOrd {
|
|
cmp : A -> A -> Ordering;
|
|
lt : A -> A -> Bool;
|
|
ge : A -> A -> Bool
|
|
};
|
|
|
|
mkOrdHelper
|
|
{A}
|
|
(cmp : A -> A -> Ordering)
|
|
{lt : A -> A -> Bool := λ {a b := isLessThan (cmp a b)}}
|
|
{gt : A -> A -> Bool := λ {a b := isGreaterThan (cmp a b)}}
|
|
: Ord A := mkOrd cmp lt gt;
|
|
|
|
ordNatNamed : Ord Nat :=
|
|
mkOrdHelper@?{
|
|
cmp := Ord.compare
|
|
};
|
|
|
|
instance
|
|
ordNat : Ord Nat := mkOrdHelper Ord.compare;
|
|
|
|
main : Nat := ite (Ord.lt 1 2) 1 0;
|