Skip to content

Instantly share code, notes, and snippets.

@krtx
Created May 31, 2017 10:26
Show Gist options
  • Save krtx/50e15937d676e549031dc871c3b4c9ca to your computer and use it in GitHub Desktop.
Save krtx/50e15937d676e549031dc871c3b4c9ca to your computer and use it in GitHub Desktop.

下の1文で ≤-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 の各フィールドにアクセスできるようにしています。これを辿ると、TotalOrderIsTotalOrderIsPartialOrderIsPreOrder と順番に open されており、IsPreorder には trans というフィールドがあるため、結果的に trans が使えるようになるという仕組みです。

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment