glossary.tex

\newglossaryentry{algebraic data type}
{
  name={algebraic data type},
  description={\todo{define}}
}

\newglossaryentry{computation rule}
{
  name={computation rule},
  description={\todo{define}}
}

\newglossaryentry{expression}
{
  name={expression},
  description={\todo{define}}
}

\newglossaryentry{first-class}
{
  name={first-class},
  description={\todo{define}}
}

\newglossaryentry{fully certified}
{
  name={fully certified},
  description={\todo{define}}
}

\newglossaryentry{function type}
{
  name={function type},
  description={\todo{define}}
}

\newglossaryentry{functional programming}
{
  name={function programming},
  description={\todo{define}}
}


\longnewglossaryentry{idris-add-clause}{
  name=\el{idris-add-clause},
  sort={idris-add-clause}
}
{
  \el{(idris-add-clause PROOF)}

  Add clauses to the declaration at point.
}

\longnewglossaryentry{idris-case-split}{
  name=\el{idris-case-split},
  sort={idris-case-split}
}
{
  \el{(idris-case-split)}

  Case split the pattern variable at point.
}

\longnewglossaryentry{idris-load-file}{
  name=\el{idris-load-file},
  sort={idris-load-file}
}
{
  \el{(idris-load-file &optional SET-LINE)}

  Pass the current buffer’s file to the inferior Idris process.

  A prefix argument restricts loading to the current line.
}

\longnewglossaryentry{idris-proof-search}{
  name=\el{idris-proof-search},
  sort={idris-proof-search}
}
{
  \el{(idris-proof-search &optional ARG)}

  Invoke the proof search. A plain prefix argument causes the
  command to prompt for hints and recursion depth, while a numeric
  prefix argument sets the recursion depth directly.
}

\newglossaryentry{induction}
{
  name={induction},
  description={\todo{define}}
}

\newglossaryentry{inductive rule}
{
  name={inductive rule},
  description={\todo{define}}
}

\newglossaryentry{module system}
{
  name={module system},
  description={\todo{define}}
}

\newglossaryentry{pattern matching}
{
  name={pattern matching},
  description={\todo{define}}
}

\newglossaryentry{polymorphic type system}
{
  name={polymorphic type system},
  description={\todo{define}}
}

\newglossaryentry{proof assistant}
{
  name={proof assistant},
  description={\todo{define}}
}

\newglossaryentry{structural recursion}
{
  name={structural recursion},
  description={\todo{define}}
}

\newglossaryentry{syntax}
{
  name=\idr{syntax},
  description={\todo{define}},
  sort={syntax}
}

\newglossaryentry{tactic}
{
  name={tactic},
  description={\todo{define}}
}

\newglossaryentry{type}
{
  name={type},
  description={\todo{define}}
}

\newglossaryentry{type system}
{
  name={type system},
  description={\todo{define}}
}

\newglossaryentry{wildcard pattern}
{
  name={wildcard pattern},
  description={\todo{define}}
}