This PR adds using syntax for constructing theories; see Algebras.jl for example usage.
The semantics for this are slightly janky. We assume that each theory that we include with using has the parent theory (i.e., when ThRing <: ThSet is the head of the theory, then ThSet is the parent) as a prefix.
We should later support more general theory inclusions.
This PR adds
using
syntax for constructing theories; see Algebras.jl for example usage.The semantics for this are slightly janky. We assume that each theory that we include with
using
has the parent theory (i.e., whenThRing <: ThSet
is the head of the theory, thenThSet
is the parent) as a prefix.We should later support more general theory inclusions.