Cheat Sheet

Inspired by the Synquid Cheat Sheet.

Refinement Terms

Term	Syntax
Arithmetic	0, 1, 2, x + y, x - y, x * y
Relation	x == y, x /= y, x < y, x <= y, x > y, x >= y
Boolean	not a, a && b, a || b a ==> b, if b then x else y

Refinement Types

Types Primitive: {Int | _v >= 0} Function: x: {Int | _v >= 0} -> y: {Int | _v >= 0} -> {Int | _v >= x && _v >= y} Datatype: {List {Int | _v >= 0} | len _v == 5} Declarations Type synonym type UPair a = {Pair a a | fst _v != snd _v} Inline predicate (formula synonym) inline abs x = if x >= 0 then x else -x Function signature: replicate :: n: Nat -> x: a -> {List a | len a == n} Function definition or synthesis goal: -- The entire function body to be synthesized: replicate = ??

-- Parts of the body to be synthesized: max = \x . \y . if x >= y then x else ?? Datatype definition: data List a where Nil :: List a Cons :: x: a -> xs: List a -> List a Measure definition: measure elems :: List a -> Set a where Nil -> [] -- One definition per constructor Cons x xs -> [x] + elems xs

-- An integer measure can be designated as the termination metric; -- measures can have postconditions (here _v >= 0): termination measure len :: List a -> {Int | _v >= 0} where Nil -> 0 Cons x xs -> 1 + len xs