Frex.Presentation

Definitions and functions dealing with single-sorted finitary signatures

Definitions

record Equation : Signature -> Type

Totality: total
Visibility: public export
Constructor: 

MkEq : {0 Sig : Signature} -> (support : Nat) -> Term Sig (Fin support) -> Term Sig (Fin support) -> Equation Sig

Projections:

.lhs : {0 Sig : Signature} -> ({rec:0} : Equation Sig) -> Term Sig (Fin (support {rec:0}))

.rhs : {0 Sig : Signature} -> ({rec:0} : Equation Sig) -> Term Sig (Fin (support {rec:0}))

.support : {0 Sig : Signature} -> Equation Sig -> Nat

Hint: 

sig1 ~> sig2 => Cast (Equation sig1) (Equation sig2)

.support : {0 Sig : Signature} -> Equation Sig -> Nat

Totality: total
Visibility: public export

support : {0 Sig : Signature} -> Equation Sig -> Nat

Totality: total
Visibility: public export

.rhs : {0 Sig : Signature} -> ({rec:0} : Equation Sig) -> Term Sig (Fin (support {rec:0}))

Totality: total
Visibility: public export

.lhs : {0 Sig : Signature} -> ({rec:0} : Equation Sig) -> Term Sig (Fin (support {rec:0}))

Totality: total
Visibility: public export

rhs : {0 Sig : Signature} -> ({rec:0} : Equation Sig) -> Term Sig (Fin (support {rec:0}))

Totality: total
Visibility: public export

lhs : {0 Sig : Signature} -> ({rec:0} : Equation Sig) -> Term Sig (Fin (support {rec:0}))

Totality: total
Visibility: public export

record Presentation : Type

Totality: total
Visibility: public export
Constructor: 

MkPresentation : (signature : Signature) -> (0 Axiom : Type) -> (Axiom -> Equation signature) -> Presentation

Projections:

0 .Axiom : Presentation -> Type

.axiom : ({rec:0} : Presentation) -> Axiom {rec:0} -> Equation (signature {rec:0})

.signature : Presentation -> Signature

Hints:

Cast (Model pres) Setoid

pres .signature = sig => Semantic (a <~.~> b) (Op sig)

pres .signature = sig => Semantic (a <~.~> b) (Term sig y)

pres .signature = sig => Semantic (Coproduct a b) (Op sig)

pres .signature = sig => Semantic (Coproduct a b) (Term sig y)

pres .signature = sig => Semantic (Extension a x) (Op sig)

pres .signature = sig => Semantic (Extension a x) (Term sig y)

pres .signature = sig => Semantic (Frex a x) (Op sig)

pres .signature = sig => Semantic (Frex a x) (Term sig y)

pres .signature = sig => Semantic (Model pres) (Op sig)

pres .signature = sig => Semantic (Model pres) (Term sig x)

pres .signature = sig => Semantic (ModelOver pres x) (Op sig)

pres .signature = sig => Semantic (ModelOver pres x) (Term sig y)

pres .signature = sig => Semantic (Free pres x) (Op sig)

pres .signature = sig => Semantic (Free pres x) (Term sig y)

Presentation -> Signature

.signature : Presentation -> Signature

Totality: total
Visibility: public export

signature : Presentation -> Signature

Totality: total
Visibility: public export

0 .Axiom : Presentation -> Type

Totality: total
Visibility: public export

0 Axiom : Presentation -> Type

Totality: total
Visibility: public export

.axiom : ({rec:0} : Presentation) -> Axiom {rec:0} -> Equation (signature {rec:0})

Totality: total
Visibility: public export

axiom : ({rec:0} : Presentation) -> Axiom {rec:0} -> Equation (signature {rec:0})

Totality: total
Visibility: public export

projectSignature : Presentation -> Signature

Totality: total
Visibility: public export

record Printer : Presentation -> Type -> Type

Totality: total
Visibility: public export
Constructor: 

MkPrinter : String -> Show (pres .Axiom) -> Printer (pres .signature) a -> Printer pres a

Projections:

.axiomShow : Printer pres a -> Show (pres .Axiom)

.sigPrinter : Printer pres a -> Printer (pres .signature) a

.theoryName : Printer pres a -> String

.theoryName : Printer pres a -> String

Totality: total
Visibility: public export

theoryName : Printer pres a -> String

Totality: total
Visibility: public export

.axiomShow : Printer pres a -> Show (pres .Axiom)

Totality: total
Visibility: public export

axiomShow : Printer pres a -> Show (pres .Axiom)

Totality: total
Visibility: public export

.sigPrinter : Printer pres a -> Printer (pres .signature) a

Totality: total
Visibility: public export

sigPrinter : Printer pres a -> Printer (pres .signature) a

Totality: total
Visibility: public export

withLower : Printer pres a -> Printer pres a

  Used to print a definition corresponding to an axiom

Totality: total
Visibility: export

withQuoted : Printer pres a -> Printer pres a

  Used to print a context

Totality: total
Visibility: export

withNames : Printer pres () -> Printer pres (Fin n)

  Used to print a definition corresponding to an axiom

Totality: total
Visibility: export

display : Printer sig () -> Equation sig -> Doc ()

Totality: total
Visibility: export

pretty : Printer sig () -> String -> List (Doc ()) -> Equation sig -> Doc ()

Totality: total
Visibility: export

display : (pres : Presentation) -> Finite (pres .Axiom) => Finite (Op (pres .signature)) => Printer pres () -> Doc ()

Totality: total
Visibility: export

display : Printer pres () -> pres .Axiom -> Doc ()

Totality: total
Visibility: export

castEqHint : sig1 ~> sig2 => Cast (Equation sig1) (Equation sig2)

Totality: total
Visibility: public export