File tree Expand file tree Collapse file tree 1 file changed +17
-9
lines changed Expand file tree Collapse file tree 1 file changed +17
-9
lines changed Original file line number Diff line number Diff line change @@ -1145,20 +1145,28 @@ pub enum ProgramClause<I: Interner> {
1145
1145
ForAll ( Binders < ProgramClauseImplication < I > > ) ,
1146
1146
}
1147
1147
1148
+ impl < I : Interner > ProgramClauseImplication < I > {
1149
+ pub fn into_from_env_clause ( self , interner : & I ) -> ProgramClauseImplication < I > {
1150
+ if self . conditions . is_empty ( interner) {
1151
+ ProgramClauseImplication {
1152
+ consequence : self . consequence . into_from_env_goal ( interner) ,
1153
+ conditions : self . conditions . clone ( ) ,
1154
+ }
1155
+ } else {
1156
+ self
1157
+ }
1158
+ }
1159
+ }
1160
+
1148
1161
impl < I : Interner > ProgramClause < I > {
1149
1162
pub fn into_from_env_clause ( self , interner : & I ) -> ProgramClause < I > {
1150
1163
match self {
1151
1164
ProgramClause :: Implies ( implication) => {
1152
- if implication. conditions . is_empty ( interner) {
1153
- ProgramClause :: Implies ( ProgramClauseImplication {
1154
- consequence : implication. consequence . into_from_env_goal ( interner) ,
1155
- conditions : Goals :: new ( interner) ,
1156
- } )
1157
- } else {
1158
- ProgramClause :: Implies ( implication)
1159
- }
1165
+ ProgramClause :: Implies ( implication. into_from_env_clause ( interner) )
1166
+ }
1167
+ ProgramClause :: ForAll ( binders_implication) => {
1168
+ ProgramClause :: ForAll ( binders_implication. map ( |i| i. into_from_env_clause ( interner) ) )
1160
1169
}
1161
- clause => clause,
1162
1170
}
1163
1171
}
1164
1172
}
You can’t perform that action at this time.
0 commit comments