Frex.Algebra.Abstract

Definitions

bindTermMapFusion : (ren : (a -> vars)) -> (t : Term sig a) -> (env : (vars -> U alg)) -> bindTerm (map ren t) env = bindTerm t (env . ren)

Totality: total
Visibility: export

bindTermsMapFusion : (ren : (a -> vars)) -> (ts : Vect n (Term sig a)) -> (env : (vars -> U alg)) -> bindTerms (bindTerms ts (Done . ren)) env = bindTerms ts (env . ren)

Totality: total
Visibility: export

bindTermExtensional : (t : Term sig vars) -> ((v : vars) -> lhs v = rhs v) -> bindTerm t lhs = bindTerm t rhs

Totality: total
Visibility: export

bindTermsExtensional : (ts : Vect n (Term sig vars)) -> ((v : vars) -> lhs v = rhs v) -> bindTerms ts lhs = bindTerms ts rhs

Totality: total
Visibility: export

record Abstract : (sig : Signature) -> Term sig (Either a b) -> Type

Totality: total
Visibility: public export
Constructor: 

MkAbstract : (u : Term sig (Either (Fin vars) b)) -> (vals : Vect vars a) -> t = map (mapFst (\k => index k vals)) u -> Abstract sig t

Projections:

.u : ({rec:0} : Abstract sig t) -> Term sig (Either (Fin (vars {rec:0})) b)

.valid : ({rec:0} : Abstract sig t) -> t = map (mapFst (\k => index k (vals {rec:0}))) (u {rec:0})

.vals : ({rec:0} : Abstract sig t) -> Vect (vars {rec:0}) a

.vars : Abstract sig t -> Nat

.vars : Abstract sig t -> Nat

Totality: total
Visibility: public export

vars : Abstract sig t -> Nat

Totality: total
Visibility: public export

.u : ({rec:0} : Abstract sig t) -> Term sig (Either (Fin (vars {rec:0})) b)

Totality: total
Visibility: public export

u : ({rec:0} : Abstract sig t) -> Term sig (Either (Fin (vars {rec:0})) b)

Totality: total
Visibility: public export

.vals : ({rec:0} : Abstract sig t) -> Vect (vars {rec:0}) a

Totality: total
Visibility: public export

vals : ({rec:0} : Abstract sig t) -> Vect (vars {rec:0}) a

Totality: total
Visibility: public export

.valid : ({rec:0} : Abstract sig t) -> t = map (mapFst (\k => index k (vals {rec:0}))) (u {rec:0})

Totality: total
Visibility: public export

valid : ({rec:0} : Abstract sig t) -> t = map (mapFst (\k => index k (vals {rec:0}))) (u {rec:0})

Totality: total
Visibility: public export

record Abstracts : (sig : Signature) -> Vect n (Term sig (Either a b)) -> Type

Totality: total
Visibility: public export
Constructor: 

MkAbstracts : (us : Vect n (Term sig (Either (Fin vars) b))) -> (vals : Vect vars a) -> ts = map (map (mapFst (\k => index k vals))) us -> Abstracts sig ts

Projections:

.us : ({rec:0} : Abstracts sig ts) -> Vect n (Term sig (Either (Fin (vars {rec:0})) b))

.valid : ({rec:0} : Abstracts sig ts) -> ts = map (map (mapFst (\k => index k (vals {rec:0})))) (us {rec:0})

.vals : ({rec:0} : Abstracts sig ts) -> Vect (vars {rec:0}) a

.vars : Abstracts sig ts -> Nat

.vars : Abstracts sig ts -> Nat

Totality: total
Visibility: public export

vars : Abstracts sig ts -> Nat

Totality: total
Visibility: public export

.us : ({rec:0} : Abstracts sig ts) -> Vect n (Term sig (Either (Fin (vars {rec:0})) b))

Totality: total
Visibility: public export

us : ({rec:0} : Abstracts sig ts) -> Vect n (Term sig (Either (Fin (vars {rec:0})) b))

Totality: total
Visibility: public export

.vals : ({rec:0} : Abstracts sig ts) -> Vect (vars {rec:0}) a

Totality: total
Visibility: public export

vals : ({rec:0} : Abstracts sig ts) -> Vect (vars {rec:0}) a

Totality: total
Visibility: public export

.valid : ({rec:0} : Abstracts sig ts) -> ts = map (map (mapFst (\k => index k (vals {rec:0})))) (us {rec:0})

Totality: total
Visibility: public export

valid : ({rec:0} : Abstracts sig ts) -> ts = map (map (mapFst (\k => index k (vals {rec:0})))) (us {rec:0})

Totality: total
Visibility: public export

(::) : Abstract sig t -> Abstracts sig ts -> Abstracts sig (t :: ts)

Totality: total
Visibility: export
Fixity Declaration: infixr operator, level 7

mkAbstract : (t : Term sig (Either a (Fin n))) -> Abstract sig t

Totality: total
Visibility: export

mkAbstracts : (ts : Vect len (Term sig (Either a (Fin n)))) -> Abstracts sig ts

Totality: total
Visibility: export