Agda.Utils.Warshall

type Matrix a

warshall

type AdjList node edge

warshallG

data Weight

inc

# flexible variables (with identifiers drawn from Int),

# rigid variables (also identified by Ints), or

# constants (like 0, infinity, or anything between)

data Node

data Rigid

type NodeId

type RigidId

type FlexId

type Scope

infinite

isBelow

data Constraint

type Constraints

emptyConstraints

data Graph

initGraph

type GM

addFlex

addNode

addEdge

addConstraint

buildGraph

mkMatrix

data LegendMatrix a b c

type Solution

emptySolution

extendSolution

data SizeExpr

sizeRigid

solve

genGraph

data Distance

genGraph_

lookupEdge

edges

prop_smaller

newEdge

genPath

prop_path

mapNodes

prop_disjoint

prop_stable

tests