# `ShotDs.Hol.Dsl`
[🔗](https://github.com/jcschuster/ShotDs/blob/v1.0.0/lib/shot_ds/hol/dsl.ex#L1)

Introduces a domain specific language (DSL) for constructing HOL terms.

The DSL utilizes unused Elixir operators with the following precedence:

      (Highest)    ~>, <~>    [Implication, Equivalence]
                   &&&        [Conjunction]
      (Lowest)     |||        [Disjunction]

> #### Note {: .info}
>
> All operators are left-associative, so `a ~> b ~> c` parses as
> `(a ~> b) ~> c`.

> #### Warning {: .warning}
>
> The operator `&&&` and `|||` will clash with the operators defined in the
> `Bitwise` module. Consider hiding these definitions when importing
> `Bitwise`.

# `const`

Primitive term representing a constant symbol of the given type.

# `var`

Primitive term representing a variable symbol of the given type.

# `neg`

```elixir
@spec neg(ShotDs.Data.Term.term_id()) :: ShotDs.Data.Term.term_id()
```

Logical Negation

# `&&&`

```elixir
@spec ShotDs.Data.Term.term_id() &amp;&amp;&amp; ShotDs.Data.Term.term_id() ::
  ShotDs.Data.Term.term_id()
```

Logical Conjunction

# `<~>`

```elixir
@spec ShotDs.Data.Term.term_id() &lt;~&gt; ShotDs.Data.Term.term_id() ::
  ShotDs.Data.Term.term_id()
```

Logical Equivalence

# `|||`

```elixir
@spec ShotDs.Data.Term.term_id() ||| ShotDs.Data.Term.term_id() ::
  ShotDs.Data.Term.term_id()
```

Logical Disjunction

# `~>`

```elixir
@spec ShotDs.Data.Term.term_id() ~&gt; ShotDs.Data.Term.term_id() ::
  ShotDs.Data.Term.term_id()
```

Logical Implication

# `eq`

```elixir
@spec eq(ShotDs.Data.Term.term_id(), ShotDs.Data.Term.term_id()) ::
  ShotDs.Data.Term.term_id()
```

Logical Equality.

Automatically infers the Hol type by inspecting the left argument's term in
the ETS cache.

# `neq`

```elixir
@spec neq(ShotDs.Data.Term.term_id(), ShotDs.Data.Term.term_id()) ::
  ShotDs.Data.Term.term_id()
```

Logical Inequality.

Automatically infers the Hol type by inspecting the left argument's term in
the ETS cache.

# `app`

```elixir
@spec app(
  ShotDs.Data.Term.term_id(),
  [ShotDs.Data.Term.term_id()] | ShotDs.Data.Term.term_id()
) ::
  ShotDs.Data.Term.term_id()
```

Applies a term to a single argument term or list of argument terms.

Temporary fresh free variables will be generated corresponding to the types.
Passes the generated variable term IDs to the provided `body_fn`. The arity of
`body_fn` must correspond to the number of given variables.

# `exists`

```elixir
@spec exists([ShotDs.Data.Type.t()] | ShotDs.Data.Type.t(), (... -&gt;
                                                         ShotDs.Data.Term.term_id())) ::
  ShotDs.Data.Term.term_id()
```

Existential quantification. Supports single or multiple variables.

Temporary fresh free variables will be generated corresponding to the types.
Passes the generated variable term IDs to the provided `body_fn`. The arity of
`body_fn` must correspond to the number of given variables.

## Examples

    iex> exists(Type.new(:i), fn x -> ... end)

    iex> exists([Type.new(:o, [:o, :o]), Type.new(:o), Type.new(:o)], fn r, x, y -> ... end)

# `forall`

```elixir
@spec forall([ShotDs.Data.Type.t()] | ShotDs.Data.Type.t(), (... -&gt;
                                                         ShotDs.Data.Term.term_id())) ::
  ShotDs.Data.Term.term_id()
```

Universal quantification. Supports single or multiple variables.

## Examples

    iex> forall(Type.new(:i), fn x -> ... end)

    iex> forall([Type.new(:o, [:o, :o]), Type.new(:o), Type.new(:o)], fn r, x, y -> ... end)

# `lambda`

```elixir
@spec lambda([ShotDs.Data.Type.t()] | ShotDs.Data.Type.t(), (... -&gt;
                                                         ShotDs.Data.Term.term_id())) ::
  ShotDs.Data.Term.term_id()
```

Constructs a lambda abstraction over a list of variable types.

Temporary fresh free variables will be generated corresponding to the types.
Passes the generated variable term IDs to the provided `body_fn`. The arity of
`body_fn` must correspond to the number of given variables.

## Examples:

    iex> lambda(Type.new(:i), fn x -> ... end)

    iex> lambda([Type.new(:o), Type.new(:o), Type.new(:o)], fn x, y, z -> ... end)

---

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