Source/Packages

Representation.Schema

packages/representations/src/Representation/Schema.alpha

701 lines99 declarations24.8 KiBSHA-256 209c8ba5712e

def · lines 208–223

parameterSchemaHasCollision

Full file
True exactly when two schema entries claim the same structural path.
208def parameterSchemaHasCollision =
209  (lambda unrestricted schemas : (family StdList (family ParameterSchema)) .
210    (eliminate
211      StdList
212      (lambda unrestricted current : (family StdList (family ParameterSchema)) . (family StdBool))
213      schemas
214      (branch StdListEmpty . (constructor StdBool StdFalse))
215      (branch
216        StdListCons
217        head
218        tail
219        induction
220        .
221        (stdBoolOr
222          (parameterSchemaContainsIdentity (parameterSchemaIdentityOf head) tail)
223          induction))))

The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.