diff options
| author | Josh Chen | 2018-06-12 12:30:54 +0200 |
|---|---|---|
| committer | Josh Chen | 2018-06-12 12:30:54 +0200 |
| commit | 91efce41a2319a9fb861ff26d7dc8c49ec726d4c (patch) | |
| tree | fd42310d712143e0f3dceff7009309a89b787b92 /HoTT.thy | |
| parent | 593faab277de53cbe2cb0c2feca5de307d9334ac (diff) | |
Type rules now have \"all\" premises explicitly stated, matching the formulation in the HoTT book.
Diffstat (limited to '')
| -rw-r--r-- | HoTT.thy | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/HoTT.thy b/HoTT.thy new file mode 100644 index 0000000..405364e --- /dev/null +++ b/HoTT.thy @@ -0,0 +1,15 @@ +(* Title: HoTT/HoTT.thy + Author: Josh Chen + +Load all the component modules for the HoTT logic. +*) + +theory HoTT imports + HoTT_Base + Prod Sum + +begin + +\<comment> \<open>Maybe tactic setup can go in here?\<close> + +end
\ No newline at end of file |