この質問の私の貧しい表現のために謝罪、私はそれを適切に尋ねる語彙を持っているか分からない。 私は（ごく最近） ⟦let x = x in x⟧ = ⊥
に似て何かを書きましたが、本当に私はここでトリッキーな何かを理解するために失敗しています。私はこのステートメントが本当に⊥であると主張することができます。なぜなら、それは非生産的な無限ループだからです。さらに、私は ⟦let ones = 1:
私は2つのほとんど同じ言語（fooとbar）に定義： theory SimpTr
imports Main
begin
type_synonym vname = "string"
type_synonym 'a env = "vname ⇒ 'a option"
datatype foo_exp =
FooBConst bool |
FooIConst i