tests-by-syntax.md

Tests By Syntax

This file lists up-to-date examples of Liquid Haskell syntax. It's guaranteed to be up-to-date since the examples are all test cases!

You may find this list useful if the main documentation becomes out of date with the latest version of Liquid Haskell.

It does not intend to explain the features that the syntax implements.

Basics

Refining Type Expressions

Float.hs inc02.hs Compose.hs

Refining Data Delcarations

Data01.hs NewType.hs Date.hs

Creating Liquid Type Synonyms

Inc03Lib.hs alias03.hs

Measures

Built-In Measures

Len01.hs

Measures Backed by Custom Haskell Functions

fst00.hs GList00Lib.hs

Measures Not Backed By Haskell Functions

AbsMeasure.hs

Checking Termination

Automatic

Ackermann.hs AutoTerm.hs StructSecondArg.hs

Manual

list00-local.hs list03.hs LocalTermExpr.hs Papp00.hs

Annotating Datatypes

AutoTerm.hs list03.hs

Abstract Refinements

Binding in Data Declaration

Map.hs deptup0.hs deptupW.hs state00.hs

Binding via forall

Papp00.hs deptupW.hs state00.hs

Binding via lambdas

Map.hs ListISort.hs ListQSort.hs deppair2.hs

Application

Map.hs ListISort.hs ListQSort.hs deptup0.hs deppair2.hs state00.hs VectorLoop.hs

Multi-Parameter Abstract Refinements

Map.hs VectorLoop.hs deppair2.hs

Proofs

Fully Automated

ple0.hs

More Manual

Compiler.hs NegNormalForm.hs

Use Curly Braces

ple0.hs Compiler.hs NegNormalForm.hs

Misc.

Defining Predicates (DEPRECATED in favor of measures)

alias04.hs

Inlining Functions (DEPRECATED in favor of measures)

alias05.hs Date.hs DoubleLit.hs

Reflecting Functions

Ple1Lib.hs ple00.hs ReflString1.hs

using ... as ...

Using00.hs

autosize Keyword

tests/pos/AutoSize.hs

LIQUID pragmas

TODO (for now, use GitHub search)