open-record-agda.md

下の１文で ≤-trans が使える理由

open DecTotalOrder decTotalOrder using () renaming (trans to ≤-trans)

レコード型のあるフィールドにアクセスするためには 型名.射影関数そのレコード型の値 と書く必要があります。

open import Data.Nat

record SomeRecord : Set where
  field
    a : ℕ
    b : ℕ

someRecord : SomeRecord
someRecord = record { a = 10 ; b = 20 }

x : ℕ
x = SomeRecord.a someRecord

ですが、open 型名値 と書くことにより、その型の射影関数を記述することで対象としている値の該当するフィールドに直接アクセスできるようになります。

open SomeRecord someRecord

y : ℕ
y = b -- 20

http://agda.readthedocs.io/en/v2.5.2/language/record-types.html#record-modules に記述があります。おそらく、レコード型に特有の文法のように思えます。

Record modules
Along with a new type, a record declaration also defines a module containing the projection functions. This allows records to be "opened", bringing the fields into scope. For instance

swap : {A B : Set} → Pair A B → Pair B A
swap p = snd , fst
  where open Pair p

もとに戻って、DecTotalOrder は内部で TotalOrder の値 totalorder をもっており、open TotalOrder totalOrder public using (poset; preorder) により totalOrder の各フィールドにアクセスできるようにしています。これを辿ると、TotalOrder → IsTotalOrder → IsPartialOrder → IsPreOrder と順番に open されており、IsPreorder には trans というフィールドがあるため、結果的に trans が使えるようになるという仕組みです。

krtx/open-record-agda.md