2.9.2. СОПОСТАВЛЕНИЕ С ЖЕСТКИМ ВЫРАЖЕНИЕМ

Любое жесткое выражение He представляет собой частный случай образцового выражения. Его особенностью является то, что для любого объектного выражения Oe либо сопоставление Oe с He невозможно, либо может быть сделано только одним способом. Таким образом, имеет место либо

{} |- Oe : He => [ ], либо

{} |- Oe : He => [Env].

Запись Env |- Oe :: He => Env' будет означать, что {} |- Oe : He => Env" и Env' = Env+Env", т.е. что Env' получается из Env следующим образом. Сначала Ое сопоставляется с He в пустой среде. Т.е. прежние значения переменных игнорируются. В результате получается среда Env", которая содержит значения для переменных из He. После этого исходная среда Env корректируется в соответствии с новыми значениями переменных из He, в результате чего получается новая среда Env'.