# `ShotDs.Data.Declaration`
[🔗](https://github.com/jcschuster/ShotDs/blob/v1.0.0/lib/shot_ds/data/declaration.ex#L1)

Represents free and bound variables as well as constants.

# `bound_var_t`

```elixir
@type bound_var_t() :: %ShotDs.Data.Declaration{
  kind: :bv,
  name: pos_integer(),
  type: ShotDs.Data.Type.t()
}
```

Type of a bound variable declaration.

# `const_name_t`

```elixir
@type const_name_t() :: String.t() | reference()
```

The name of a constant is given as a string or a reference (indicating a
generated fresh constant).

# `const_t`

```elixir
@type const_t() :: %ShotDs.Data.Declaration{
  kind: :co,
  name: const_name_t(),
  type: ShotDs.Data.Type.t()
}
```

Type of a constant declaration.

# `free_var_t`

```elixir
@type free_var_t() :: %ShotDs.Data.Declaration{
  kind: :fv,
  name: var_name_t(),
  type: ShotDs.Data.Type.t()
}
```

Type of a free variable declaration.

# `t`

```elixir
@type t() :: free_var_t() | bound_var_t() | const_t()
```

The type of a declaration. A declaration represents either a free variable, a
bound variable or a constant.

# `var_name_t`

```elixir
@type var_name_t() :: String.t() | reference() | pos_integer()
```

The name of a free variable is given as a string, a reference (indicating a
generated fresh variable) or a positive integer representing its de Bruijn
index.

# `format`

```elixir
@spec format(t(), boolean()) :: String.t()
```

Pretty-prints a declaration.

# `fresh_const`

```elixir
@spec fresh_const(ShotDs.Data.Type.t()) :: const_t()
```

Generates a fresh constant of the given type using Erlang references to
ensure uniqueness. Useful for skolemization.

# `fresh_var`

```elixir
@spec fresh_var(ShotDs.Data.Type.t()) :: free_var_t()
```

Generates a fresh variable of the given type using Erlang references to
ensure uniqueness. Useful for γ-instantiations in tableaux.

> #### Note {: .info}
>
> Consider wrapping functions using this to create temporary free variables
> with `ShotDs.Stt.TermFactory.with_scratchpad/1` or
> `ShotDs.Stt.TermFactory.with_scratchpad!/1` for garbage collection.

# `new_const`

```elixir
@spec new_const(const_name_t(), ShotDs.Data.Type.t()) :: const_t()
```

Returns a struct representing a constant of the given name and type.

# `new_free_var`

```elixir
@spec new_free_var(var_name_t(), ShotDs.Data.Type.t()) :: free_var_t()
```

Returns a struct representing a free variable of the given name and type.

---

*Consult [api-reference.md](api-reference.md) for complete listing*