Check-in [caa7fbdd73]

Not logged in

Many hyperlinks are disabled.
Use anonymous login to enable hyperlinks.

Overview
Comment:Added screen shot of the proof assistant, starting a proof.
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:caa7fbdd73265ada6bb170a4871b156b529268ce
User & Date: andy 2015-04-15 11:44:40
Context
2015-04-15
11:47
Split the `What` argument to elaborate into `What` and `Data`. What is now either 'goal' or 'ctx', while data identifies the sub-element. For ctx this is the index, but it can also be the index of a disjunct (when the goal is a disjunction), or 'ih' to indicate backchaining the user goal on the IH instead of on its definitions. check-in: 9e954b6b56 user: andy tags: trunk
11:44
Added screen shot of the proof assistant, starting a proof. check-in: caa7fbdd73 user: andy tags: trunk
11:12
Added some utilities for working with proof terms (extracting subproofs, getting proof goals, navigating through proofs on a path, etc.) check-in: e902cf4ec5 user: andy tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to report/arend-report.tex.

959
960
961
962
963
964
965











966
967
968
969
970
971
972
\includegraphics[width=6.5in]{repl-sample.png}
\end{centering}

\caption{The browser-based run-eval-print-loop interface}
\label{fig:repl}
\end{figure*}













\clearpage
\section{Implementation}

\newthought{Arend currently exists} in two semi-overlapping implementations:
\begin{itemize}
\item A \emph{client-based} implementation, written in JavaScript and running







>
>
>
>
>
>
>
>
>
>
>







959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
\includegraphics[width=6.5in]{repl-sample.png}
\end{centering}

\caption{The browser-based run-eval-print-loop interface}
\label{fig:repl}
\end{figure*}


\begin{figure*}[ht!]

\begin{centering}
\includegraphics[width=6.5in]{proof-start-sample.png}
\end{centering}

\caption{The proof assistant interface, with an incomplete inductive proof}
\label{fig:passist1}
\end{figure*}


\clearpage
\section{Implementation}

\newthought{Arend currently exists} in two semi-overlapping implementations:
\begin{itemize}
\item A \emph{client-based} implementation, written in JavaScript and running

Added report/proof-start-sample.png.

cannot compute difference between binary files