Frex.Free.Construction.Linear

Definitions

.bindTerm : (a : PresetoidAlgebra sig) -> Term sig x -> (x -> U a) -> U a

Totality: total
Visibility: public export

data Step : (pres : Presentation) -> (a : PresetoidAlgebra (pres .signature)) -> Rel (U a)

Totality: total
Visibility: public export
Constructors:

Include : a .relation x y -> Step pres a x y

ByAxiom : (eq : Axiom pres) -> (env : (Fin ((pres .axiom eq) .support) -> U a)) -> Step pres a (a .bindTerm ((pres .axiom eq) .lhs) env) (a .bindTerm ((pres .axiom eq) .rhs) env)

display : Show (a .relation x y) => Show (pres .Axiom) => Step pres a x y -> Doc ()

Totality: total
Visibility: export

displayNamed : Bool -> Printer pres () -> Step pres (QuotientData pres (cast (Fin n))) x y -> Doc ()

Totality: total
Visibility: export

plug : (a : Algebra sig) -> Term sig (Maybe (U a)) -> U a -> U a

Totality: total
Visibility: public export

(:.:) : Term sig (Maybe a) -> Term sig (Maybe a) -> Term sig (Maybe a)

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 0

plugFusion : (ctx2 : Term sig (Maybe (U a))) -> (ctx1 : Term sig (Maybe (U a))) -> (t : U a) -> plug a ctx2 (plug a ctx1 t) = plug a (ctx2 :.: ctx1) t

Totality: total
Visibility: export

data Locate : (sig : Signature) -> (a : Algebra sig) -> Rel (U a) -> Rel (U a)

Totality: total
Visibility: public export
Constructors:

Here : r x y -> Locate sig a r x y

  We prove the equality by invoking a rule at the
  toplevel

Cong : (t : Term sig (Maybe (U a))) -> r lhs rhs -> Locate sig a r (plug a t lhs) (plug a t rhs)

  We focus on a subterm `lhs` that may appear in
  multiple locations and rewrite it to `rhs` using a
  specific rule.

0 Closure : (pres : Presentation) -> (a : PresetoidAlgebra (pres .signature)) -> Rel (U a)

Totality: total
Visibility: public export

0 Derivation : (p : Presentation) -> (a : PresetoidAlgebra (p .signature)) -> Rel (U a)

Totality: total
Visibility: public export

0 Proof : (pres : Presentation) -> Term (pres .signature) (Fin n) -> Term (pres .signature) (Fin n) -> Type

Totality: total
Visibility: public export

join : Locate sig alg (Locate sig alg r) ~> Locate sig alg r

Totality: total
Visibility: export

locate : Locate (pres .signature) (a .algebra) (Derivation pres a) ~> Derivation pres a

Totality: total
Visibility: export

linearise : Maybe (DecEq (U a)) -> ((a |-)) ~> Derivation pres a

Totality: total
Visibility: export

record Focus : (sig : Signature) -> Algebra sig -> Type

Totality: total
Visibility: public export
Constructor: 

MkFocus : Term sig (Maybe (U a)) -> U a -> Focus sig a

Projections:

.content : Focus sig a -> U a

.context : Focus sig a -> Term sig (Maybe (U a))

.context : Focus sig a -> Term sig (Maybe (U a))

Totality: total
Visibility: public export

context : Focus sig a -> Term sig (Maybe (U a))

Totality: total
Visibility: public export

.content : Focus sig a -> U a

Totality: total
Visibility: public export

content : Focus sig a -> U a

Totality: total
Visibility: public export

display : Printer sig (U a) -> Focus sig a -> Doc ()

Totality: total
Visibility: export

unicode : Printer

Totality: total
Visibility: export

latex : Printer

Totality: total
Visibility: export

latexPreamble : String

Totality: total
Visibility: export

compactLatex : Printer

Totality: total
Visibility: export

compactLatexPreamble : String

Totality: total
Visibility: export

display : Printer -> Printer pres (U a) -> Show (a .relation x y) => Derivation pres a x y -> Doc ()

Totality: total
Visibility: export

displayPerhapsWithMagic : Printer -> Printer pres (U a) -> Show (a .relation x y) => Maybe (DecEq (U a)) -> Maybe (Ord (U a)) -> (|-) a x y -> Doc ()

Totality: total
Visibility: export

display : Printer -> Printer pres (U a) -> Show (a .relation x y) => DecEq (U a) => Ord (U a) => (|-) a x y -> Doc ()

Totality: total
Visibility: export

displayWithoutDecEq : Printer -> Printer pres (U a) -> Show (a .relation x y) => (|-) a x y -> Doc ()

Totality: total
Visibility: export