|
definition:
|
loDefTrees :: Eq f => [DefTree f] -> Term f -> Maybe (Pos, [DefTree f])
loDefTrees [] _ = Nothing
loDefTrees dts@(_:_) t = listToMaybe (loDefTrees' eps t)
where
loDefTrees' _ (TermVar _) = []
loDefTrees' p c@(TermCons _ ts)
| hasDefTree dts c = [(p, selectDefTrees dts c)]
| otherwise = [lp | (p', t') <- zip [1..] ts,
lp <- loDefTrees' (p .> [p']) t']
|
|
demand:
|
argument 2
|
|
deterministic:
|
deterministic operation
|
|
documentation:
|
--- Returns the position and the definitional trees from the given list of
--- definitional trees for the leftmost outermost defined constructor in a
--- term or `Nothing` if no such pair exists.
|
|
failfree:
|
(_, _, _)
|
|
indeterministic:
|
referentially transparent operation
|
|
infix:
|
no fixity defined
|
|
iotype:
|
{(_,{[]},_) |-> {Nothing} || (_,{:},_) |-> {Just,Nothing}}
|
|
name:
|
loDefTrees
|
|
precedence:
|
no precedence defined
|
|
result-values:
|
{Just,Nothing}
|
|
signature:
|
Prelude.Eq a => [DefTree a] -> Rewriting.Term.Term a
-> Prelude.Maybe ([Prelude.Int], [DefTree a])
|
|
solution-complete:
|
operation might suspend on free variables
|
|
terminating:
|
possibly non-terminating
|
|
totally-defined:
|
possibly non-reducible on same data term
|