Docs / Syntax / Minimalist / Copy / Reading
import Linglib.Syntax.Minimalist.Copy.Reading · namespace Minimalist.LinearizedSyntacticObject.Marked
This file defines what a linearized object with its lower copies marked gives to the semantic interface. A reading is the finite set of chains read low, a chain being named by its term in the copy object. A chain read high keeps its higher copy, and its lower copies contract to traces. A chain read low keeps its lowest copy, and its higher copies are deleted. With no chain read low the result is the contraction. A reading binds only where the copy object does, unless it deletes a copy whose sister is a copy of it.
Minimalist.LinearizedSyntacticObject.Marked.reading: the recursion over a marked tree that every
reading's objects are built by.Minimalist.LinearizedSyntacticObject.Marked.lf: the object a reading gives.Minimalist.LinearizedSyntacticObject.Marked.carrying: the chains with a lower copy holding a
token.The term of the copy object a tree is a copy of, its marks forgotten. Marking leaves it unchanged, so it names a chain at every stage of a derivation.
Used by ReadLow, isSome_lowerCopy?_iff, map_snd_eq_leaf_of_lfBy_eq, tokenCCommands_of_tokenCCommands_lfBy, cCommands_unmark_of_cCommands_lf
The mark of a lower copy of x in y: a marked subtree of y with the term of x.
The definition is too large to print here; read it in the source.
Used by reading_pair, isSome_lowerCopy?_iff, lfBy_pair, lowerCopy?_map_none
The chain of the copy r is read low in the reading low.
Built from
Used by instDecidablePredRoseTreeProdCopyMarkVertexTokenReadLow, not_readLow_empty, lfTree, cCommands_unmark_of_cCommands_lf
Used in Syntax/Minimalist/Copy/Cut
The definition is too large to print here; read it in the source.
Built from
Built from
A node with its daughters, each paired with what it reads as. A copy of a chain read low is
deleted at its movement node by del, which receives that copy and what the other daughter reads
as, and wrap goes around the other daughter of a copy of a chain read high. A marked copy reads as
tr of itself and its mark if its chain is read high.
The definition is too large to print here; read it in the source.
Used by reading, fold_readStep, reading_node
What a marked tree reads as, under readStep.
Built from
Used by fold_readStep, reading_node, reading_some, reading_of_length_ne, reading_pair
Built from ,
Built from ,
A lower copy reads as tr if its chain is read high, and otherwise as if it were not one.
Built from
Built from
A binary node, when wrap does nothing: a daughter that has a lower copy in the other is
deleted if its chain is read low.
Built from ,
Built from ,
The object a test of copies gives, as a tree of vertices.
The definition is too large to print here; read it in the source.
Used by lfTree, lfBy_some, lfBy_of_length_ne, lfBy_pair, lfBy_leaf, lfBy_node_cases, isSyntacticObject_lfBy, lfBy_map_none, holds_of_holds_lfBy, map_snd_eq_leaf_of_lfBy_eq, tokenCCommands_of_tokenCCommands_lfBy
Used in Syntax/Minimalist/Copy/Cut
The object a reading gives, as a tree of vertices.
Built from ,
Used by lf, lfTree_empty
Built from
Built from
Built from ,
Built from
The object a test gives at a node is a trace, the node with its daughters' objects, or a daughter's object.
Built from
Built from
The object a reading gives: each chain in low keeps its lowest copy, and every other its
highest, its lower copies contracted.
Built from
Used by lf_empty, lf_ofLinearized, cCommands_unmark_of_cCommands_lf
Used in Syntax/Minimalist/Copy/Cut, Syntax/Minimalist/Copy/ToTree, Collins2026
The chains with a lower copy holding y.
The definition is too large to print here; read it in the source.
Used in Syntax/Minimalist/Copy/BindingAtReading, Collins2005
Built from
With no chain read low, a reading gives the contraction.
Built from
Built from
Built from
An object with no lower copy gives itself under every reading.
Built from
A reading holds only what the copy object does.
Built from
A token is a daughter in a reading only where it is one in the copy object, when no copy the test deletes has a sister that is a copy of it.
Built from ,
A token c-commanding another in a reading does so in the copy object, when no copy the test deletes has a sister that is a copy of it.
Built from ,
Binding at a reading is binding at the copy object, when no copy the reading deletes has a sister that is a copy of it.
Built from , ,