/ test-package / JumpToRecordFieldWhenVarIsOfRecordTypeFromLamBinding.dhall
Copy path to clipboardOn this example, dhall-docs
will detect that the argument a
of the only
function in this file is of record type. Therefore, any interactions on selector
expressions over the a
variable will interact with the fields on the record-type.
Note that the treatment for Lam
variables is different from Let
bindings:
the annotation doesn't affect on the later case. This can be seen in the
test case for let bindings
Source
{-|
On this example, `dhall-docs` will detect that the argument `a` of the only
function in this file is of record type. Therefore, any interactions on selector
expressions over the `a` variable will interact with the fields on the record-type.
Note that the treatment for `Lam` variables is different from `Let` bindings:
the annotation doesn't affect on the later case. This can be seen in the
[test case for let bindings](./JumpToRecordFieldWhenLetAnnotationPresentShouldIgnoreAnnotation.dhall)
-}
λ(b : Type) →
λ(c : Type) →
λ(a : { list : List b, cons : b → c → c, nil : c }) →
List/fold b a.list c a.cons a.nil