File tree 2 files changed +7
-2
lines changed
reference/contextual-witnesses
2 files changed +7
-2
lines changed Original file line number Diff line number Diff line change @@ -146,6 +146,9 @@ FunType ::= FunArgTypes ‘=>’ Type
146
146
FunArgTypes ::= InfixType
147
147
| ‘(’ [ ‘[given]’ FunArgType {‘,’ FunArgType } ] ‘)’
148
148
| ‘(’ ‘[given]’ TypedFunParam {‘,’ TypedFunParam } ‘)’
149
+ GivenArgs ::= InfixType
150
+ | ‘(’ [ FunArgType {‘,’ FunArgType } ] ‘)’
151
+ | ‘(’ ‘val’ TypedFunParam {‘,’ ‘val’ TypedFunParam } ‘)’
149
152
TypedFunParam ::= id ‘:’ Type
150
153
MatchType ::= InfixType `match` ‘{’ TypeCaseClauses ‘}’
151
154
InfixType ::= RefinedType {id [nl] RefinedType} InfixOp(t1, op, t2)
Original file line number Diff line number Diff line change @@ -13,11 +13,12 @@ trait Ord[T] {
13
13
def (x : T ) > (y : T ) = compare(x, y) > 0
14
14
}
15
15
16
- witness intOrd of Ord [Int ] with
16
+ witness intOrd of Ord [Int ] {
17
17
def compare (x : Int , y : Int ) =
18
18
if (x < y) - 1 else if (x > y) + 1 else 0
19
+ }
19
20
20
- witness listOrd[T ](given ord : Ord [T ]) of Ord [List [T ]] with
21
+ witness listOrd[T ](given ord : Ord [T ]) of Ord [List [T ]] {
21
22
22
23
def compare (xs : List [T ], ys : List [T ]): Int = (xs, ys) match
23
24
case (Nil , Nil ) => 0
@@ -26,6 +27,7 @@ witness listOrd[T](given ord: Ord[T]) of Ord[List[T]] with
26
27
case (x :: xs1, y :: ys1) =>
27
28
val fst = ord.compare(x, y)
28
29
if (fst != 0 ) fst else compare(xs1, ys1)
30
+ }
29
31
```
30
32
This code defines a trait ` Ord ` with two witnesses. ` intOrd ` defines
31
33
a witness of the type ` Ord[Int] ` whereas ` listOrd[T] ` defines witnesses
You can’t perform that action at this time.
0 commit comments