forked from dafny-lang/dafny
-
Notifications
You must be signed in to change notification settings - Fork 0
Open
Description
- 순서가 바뀌는 경우
- 입력:
datatype D = A | B | ghost C
method m(d: D) returns (r: bool) {
r := match d {
case A =>true
case B =>true
case C =>true
};
}
- 출력:
method m(d: D) returns (r: bool)
{
r := match d { case A => true case B => true case C => true };
}
datatype D = A | B | ghost C
- 순서가 유지되는 경우
- 입력:
method m(d: D) returns (r: bool) {
r := match d {
case A =>true
case B =>true
case C =>true
};
}
datatype D = A | B | ghost C
- 출력: 동일
Reactions are currently unavailable
Metadata
Metadata
Assignees
Labels
No labels