Packages

shot_ds

1.2.2
1.2.6 1.2.5 1.2.4 1.2.3 1.2.2 1.2.1 1.2.0 1.1.8 1.1.7 1.1.6 1.1.5 1.1.4 1.1.3 1.1.2 1.1.1 1.1.0 1.0.5 1.0.4 1.0.3 1.0.2 1.0.1 1.0.0 0.5.0 0.4.2 0.4.1 0.4.0 0.3.3 0.3.2 0.3.1 0.3.0 0.2.3 0.2.2 0.2.1 0.2.0 0.1.2 0.1.1 0.1.0

Data structures for various HOL objects and TH0/1 parser.

HexDocs

Current section

Files

Jump to
Readme
37 Versions
1 Dependency
Dependants
Files
Activity
shot_ds lib shot_ds data substitution.ex
Raw

lib/shot_ds/data/substitution.ex 

defmodule ShotDs.Data.Substitution do

  @moduledoc """

  Represents a substitution.

  """



  alias ShotDs.Data.{Declaration, Term}



  @enforce_keys [:fvar, :term_id]

  defstruct [:fvar, :term_id]



  @typedoc """

  The type of a substitution.



  A substitution is made up by the free variable to substitute and the id for

  its replacement term.

  """

  @type t :: %__MODULE__{

          fvar: Declaration.free_var_t(),

          term_id: Term.term_id()

        }



  @doc """

  Creates a new substitution for the given free variable and the id for its

  replacement term.

  """

  @spec new(Declaration.free_var_t(), Term.term_id()) :: t()

  def new(%Declaration{kind: :fv} = fvar, term_id) when is_integer(term_id) do

    %__MODULE__{fvar: fvar, term_id: term_id}

  end

end