-
Notifications
You must be signed in to change notification settings - Fork 1.9k
Closed
Labels
S-actionableSomeone could pick this issue up and work on it right nowSomeone could pick this issue up and work on it right now
Description
The keywords seem to have precedence? For example:
For the following code:
/// Synthesize the type of a term.
#[debug_ensures(self.universe_offset == old(self.universe_offset))]
#[debug_ensures(self.types.size() == old(self.types.size()))]
#[debug_ensures(self.values.size() == old(self.values.size()))]
pub fn synth_type(&mut self, term: &Term) -> Arc<Value> {
match &term.data {
TermData::Global(name) => match self.globals.get(name) {
Some((r#type, _)) => self.eval_term(r#type),
None => {
self.report(CoreTypingMessage::UnboundGlobal {
name: name.to_owned(),
});
Arc::new(Value::Error)
}
},
TermData::Local(index) => match self.types.get(*index) {
Some(r#type) => r#type.clone(),
None => {
self.report(CoreTypingMessage::UnboundLocal);
Arc::new(Value::Error)
}
},
TermData::Ann(term, r#type) => {
self.is_type(r#type);
let r#type = self.eval_term(r#type);
self.check_type(term, &r#type);
r#type
}Metadata
Metadata
Assignees
Labels
S-actionableSomeone could pick this issue up and work on it right nowSomeone could pick this issue up and work on it right now
