Safe Haskell | None |
---|
- displayForm :: QName -> Args -> TCM (Maybe DisplayTerm)
- matchDisplayForm :: DisplayForm -> Args -> MaybeT TCM DisplayTerm
- class Match a where
Documentation
displayForm :: QName -> Args -> TCM (Maybe DisplayTerm)Source
Find a matching display form for q vs
.
In essence this tries to reqwrite q vs
with any
display form q ps --> dt
and returns the instantiated
dt
if successful. First match wins.
matchDisplayForm :: DisplayForm -> Args -> MaybeT TCM DisplayTermSource
Match a DisplayForm
q ps = v
against q vs
.
Return the DisplayTerm
v[us]
if the match was successful,
i.e., vs / ps = Just us
.
Class Match
for matching a term p
in the role of a pattern
against a term v
.
The 0th variable in p
plays the role
of a place holder (pattern variable). Each occurrence of
var 0
in p
stands for a different pattern variable.
The result of matching, if successful, is a list of solutions for the pattern variables, in left-to-right order.
The 0th variable is in scope in the input v
, but should not
actually occur!
In the output solution, the 0th
variable is no longer in scope.
(It has been substituted by __IMPOSSIBLE__ which corresponds to
a raise by -1).