Skip to content

Commit ab81660

Browse files
authored
Use field names while creating EvalOpts (idris-lang#3649)
1 parent 8695f06 commit ab81660

File tree

1 file changed

+40
-4
lines changed

1 file changed

+40
-4
lines changed

src/Core/Value.idr

Lines changed: 40 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -27,19 +27,55 @@ record EvalOpts where
2727

2828
export
2929
defaultOpts : EvalOpts
30-
defaultOpts = MkEvalOpts False False True False False Nothing [] CBN
30+
defaultOpts = MkEvalOpts
31+
{ holesOnly = False
32+
, argHolesOnly = False
33+
, removeAs = True
34+
, evalAll = False
35+
, tcInline = False
36+
, fuel = Nothing
37+
, reduceLimit = []
38+
, strategy = CBN
39+
}
3140

3241
export
3342
withHoles : EvalOpts
34-
withHoles = MkEvalOpts True True False False False Nothing [] CBN
43+
withHoles = MkEvalOpts
44+
{ holesOnly = True
45+
, argHolesOnly = True
46+
, removeAs = False
47+
, evalAll = False
48+
, tcInline = False
49+
, fuel = Nothing
50+
, reduceLimit = []
51+
, strategy = CBN
52+
}
3553

3654
export
3755
withAll : EvalOpts
38-
withAll = MkEvalOpts False False True True False Nothing [] CBN
56+
withAll = MkEvalOpts
57+
{ holesOnly = False
58+
, argHolesOnly = False
59+
, removeAs = True
60+
, evalAll = True
61+
, tcInline = False
62+
, fuel = Nothing
63+
, reduceLimit = []
64+
, strategy = CBN
65+
}
3966

4067
export
4168
withArgHoles : EvalOpts
42-
withArgHoles = MkEvalOpts False True False False False Nothing [] CBN
69+
withArgHoles = MkEvalOpts
70+
{ holesOnly = False
71+
, argHolesOnly = True
72+
, removeAs = False
73+
, evalAll = False
74+
, tcInline = False
75+
, fuel = Nothing
76+
, reduceLimit = []
77+
, strategy = CBN
78+
}
4379

4480
export
4581
tcOnly : EvalOpts

0 commit comments

Comments
 (0)