Agda-2.3.0: A dependently typed functional programming language and proof assistant

Agda.TypeChecking.Positivity

Description

Check that a datatype is strictly positive.

Synopsis

Documentation

checkStrictlyPositive :: MutualId -> TCM ()Source

Check that the datatypes in the given mutual block are strictly positive.

data OccursWhere Source

Description of an occurrence.

Constructors

LeftOfArrow OccursWhere 
DefArg QName Nat OccursWhere

in the nth argument of a define constant

VarArg OccursWhere

as an argument to a bound variable

MetaArg OccursWhere

as an argument of a metavariable

ConArgType QName OccursWhere

in the type of a constructor

InClause Nat OccursWhere

in the nth clause of a defined function

InDefOf QName OccursWhere

in the definition of a constant

Here 
Unknown

an unknown position (treated as negative)

data Item Source

Constructors

AnArg Nat 
ADef QName 

Instances

computeOccurrences :: QName -> TCM OccurrencesSource

Compute the occurrences in a given definition.

etaExpandClause :: Nat -> Clause -> ClauseSource

Eta expand a clause to have the given number of variables. Warning: doesn't update telescope or permutation! This is used instead of special treatment of lambdas (which was unsound: issue 121)

data Edge Source

Instances

computeEdge :: Set QName -> OccursWhere -> TCM (Node, Edge)Source

Given an OccursWhere computes the target node and an Edge. The first argument is the set of names in the current mutual block.