That should hopefully add it to the generated TOC.

This change imports the wiki contents and use sphinx to render
an HTML website. The main featur...

This changes the formatting of Dhall source files affected
by dhall-lang/dhall-haskell#183
or ...

This is motivated by the following discussion:

https://github.com/dhall-lang/dhall-haskell/is...

In #745 we changed annotated expressions to return the inferred type,
not the annotated type, b...

Inspired by dhall-lang/dhall-haskell#1383.

@Gabriel439 had discovered in
https://github.com/dhall-lang/dhall-haskell/pull/1500
that we we...

Both @philandstuff and @weeezes kindly informed me that I had accidentally
checked in a secret ...

Fixes https://github.com/dhall-lang/dhall-lang/issues/783

* abs : Integer -> Natural (Absolute value)
* clamp : Integer -> Natural (Clamp negatives to ...

* Implement a debugging utility JSON/renderYAML for rendering JSON to YAML, similar to JSON/rend...

... so we can't keep forgetting to keep it up to date

This also updates the `generate-diagnos...

This `README` discusses how to use and contribute to the Prelude

* Define forall together with the other keywords, instead of
with the operators
* Add forall...

The Haskell implementation currently gets this wrong. See
https://github.com/dhall-lang/dhall-h...

The fusion rules do not trigger reliably (i.e. they are not confluent),
and they complicate the...

Now that we have an efficient `Natural/subtract` we can implement an
efficient `List/{take,drop}`

This is one step towards moving more `dhall-to-json` functionality into pure
Dhall. This imple...

The deleted test causes the Prelude to fail when imported remotely
due to failing the referenti...

* Remove unnecessary `nixpkgs` input (See:
https://github.com/dhall-lang/dhall-haskell/pull/1...

Most of the README is superseded by the integrations page which contains
up-to-date information...

Fixes https://github.com/dhall-lang/dhall-lang/issues/382

This adds a new record completion o...

JSON.key{Text,Value} initially remain as re-exports, but will
eventually be removed.

Fixes #...

Related to #512

This change adds support for leading (but not trailing) commas and bars

This includes some formatting changes due to recent updates in
`dhall format`.

Fixes https://github.com/dhall-lang/dhall-lang/issues/752.

Fixes #749.

Co-Authored-By: Gabriel Gonzalez <[email protected]>

This makes it easier to ensure that failure tests aren't failing for
the wrong reasons.

Fixe...

I discovered these via a test coverage report for the Haskell
implementation.

Related to htt...

Quoting from `type-inference.md`:

> Types inferred according to the following rules will be i...

The result must of course be a type! :/

The rule is:

Γ ⊢ e :⇥ {} Γ ⊢ T₀ :⇥ Type T₀ ⇥ List { mapKey : Text, mapValue : T₁ }
...

This is an attempt to clarify what I believe the standard already
wants to say:

* Fields are...

* Fix the type of XML.attribute
* Adjust to changes from #732.

Also update the definition of...

Since there have been multiple PRs forgetting to update that test,
here is a reminder.

Context: dhall-lang/dhall-haskell#1278

Fixes #721.

* Add Natural.subtract

* Small improvements for the Natural comparison functions
- Add pro...

Fixes #661.

* Move all typecheck tests over to type-inference

* Update tests/README.md to reflect changes...

Fixes https://github.com/dhall-lang/dhall-lang/pull/705

This essentially adds a thin white border to the logo so that it can
render against dark backgr...

Since #669, dependent function types have been allowed by the function
check, but type-inferenc...

* fix tests to match beta-normalization.md

As far as I can work out, these test missed some s...

Now, e.g., `https://prelude.dhall-lang.org/v8.0.0/Optional/map` will
resolve to the version 8.0...

PR #674 added new functions to the prelude without updating this test,
which now fails. This f...

* Selecting from a record type is illegal

* Use ⩓ to typecheck ∧

* Tiny legibility improve...

Now that the "Learn Dhall in Y minutes" tutorial is live we can just
link to that (and I consid...

Currently, the standard requires implementations to URL-decode unquoted
path segments. I think...

* Make some normalization tests typecheck

* Fix operator normalization tests

* Fix types o...

Adds Natural/lessThan, Natural/lessThanEqual, Natural/equal, Natural/greaterThanEqual and Natura...

This standard change now allows records to contain terms from different universes. For example, ...

For ease of implementation, we'd like to be able to branch exclusively
on nonterminals. Here bo...

Without this, my ABNF parsing library rejected the file

* Add a bunch of tests

* Remove some now redundant tests

* Test mandatory spaces in parser...

We already have analogous rules for `||` and `&&`, which are idempotent
too.

The remaining i...

Equivalence includes β-normalization, so it's unnecessary to
normalize arguments before compari...

Background:
https://discourse.dhall-lang.org/t/whats-up-with-bool-even-and-bool-odd/54

Follow-up to #664.

This was accidentally changed to `dhall format` in #669

This turned out to be a tricky case for the Haskell implementation
(see https://github.com/dhal...

The immediate motivation for this change is to add language support for
assertions verified at ...

`a` and `b` are somewhat arbitrary expressions; `n` and `m` are natural
literals. To me it mak...

* Allow `toMap e : T` where `e` is a nonempty record

Currently, there is only one type infere...

This caught a bug in the ruby implementation.

Label 27 is for toMap expressions; we should have a test for it.

Inspired by #661.

Fixes #614.

This ensures that the `as Location` tests chain in a consistent way.
The parent ...

Label 28 is "empty lists not in the form `[] : List T`"; we should have
a test for it.