Skip to content

Commit

Permalink
Add Embeddable typeclass
Browse files Browse the repository at this point in the history
  • Loading branch information
propensive committed Oct 8, 2024
1 parent 125d1a3 commit 4f0164d
Show file tree
Hide file tree
Showing 4 changed files with 12 additions and 1 deletion.
Empty file.
7 changes: 7 additions & 0 deletions src/core/contextual.Embeddable.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
package contextual

trait Embeddable:
type Self
type Format
type Operand
def embed(value: Self): Operand
4 changes: 4 additions & 0 deletions src/core/contextual.Substitution.scala
Original file line number Diff line number Diff line change
Expand Up @@ -20,5 +20,9 @@ import language.experimental.captureChecking

import rudiments.*

object Substitution:
given [ValueType: Embeddable] => Substitution[ValueType.Operand, ValueType, "x"] =
ValueType.embed(_)

trait Substitution[InputType, -ValueType, SubstitutionType <: Label]
extends Insertion[InputType, ValueType]
2 changes: 1 addition & 1 deletion src/core/soundness+contextual-core.scala
Original file line number Diff line number Diff line change
Expand Up @@ -16,4 +16,4 @@

package soundness

export contextual.{Insertion, InterpolationError, Interpolator, Verifier, Substitution}
export contextual.{Insertion, InterpolationError, Interpolator, Verifier, Substitution, Embeddable}

0 comments on commit 4f0164d

Please # to comment.