talking about specific records in checks

[florianschanda]

We can check if a reference is null or not null. But we cannot check if a certain reference is there or not, because in the check file the symbol wouldn't be know. For example this is not valid:

checks Requirement {
  base_safety_case in trlc_links, warning "the base safety case is not mentioned"
}

We could do this through lookup functions perhaps:

checks Requirement {
  Requirement("general.base_safety_case") in trlc_links, warning "the base safety case is not mentioned"
}

So:

• each record type T introduces a str -> T function
• this function looks up the (qualified) name in the current symbol table at run-time
• specifying a requirement that does not exist creates a run-time error (like div 0)
• specifying a requirement that does not match in type creates a run-time error
• following lsp, you can of course make a view from a more specialized extension to its parent type
• but not the other way around

I do not want to permit general.base_safety_case without the sugar because then we could not spell-check check typos.