8a74105007
This begins updates the filesystem layout for the tests to match the new layout from the standard test suite (See: https://github.com/dhall-lang/dhall-lang/pull/265) This is still missing a part of the standard requirement, which is checking parsing and import test results against an expected output (instead of just checking that they succeed). I plan to add that in a subsequent pull request. This is mainly to unblock other features that require using the new standard layout.
19 lines
470 B
Plaintext
19 lines
470 B
Plaintext
{ example0 =
|
|
Natural/build
|
|
( λ(natural : Type)
|
|
→ λ(succ : natural → natural)
|
|
→ λ(zero : natural)
|
|
→ succ zero
|
|
)
|
|
, example1 =
|
|
Natural/build (λ(x : Type) → λ(x : x → x) → λ(x : x@1) → x@1 x)
|
|
, example2 =
|
|
λ(id : ∀(a : Type) → a → a)
|
|
→ Natural/build
|
|
( λ(natural : Type)
|
|
→ λ(succ : natural → natural)
|
|
→ λ(zero : natural)
|
|
→ id natural (succ zero)
|
|
)
|
|
}
|