Commit 6b140986 authored by jfschaefer's avatar jfschaefer

switch to Teaching

parent 0cc526f6
id: teaching/lbs1920
narration-base: http://mathhub.info/teaching/lbs1920
id: Teaching/lbs1920
narration-base: http://mathhub.info/Teaching/lbs1920
......@@ -13313,7 +13313,7 @@ You can achieve this using an extra lambda expression (i.e. <code>[x] (happy' x)
<div class="prompt input_prompt">In&nbsp;[&nbsp;]:</div>
<div class="inner_cell">
<div class="input_area">
<div class=" highlight hl-gf"><pre><span></span>view A3SemanticsConstruction : http://mathhub.info/teaching/lbs1920/Assignment3.gf?Assignment3 -&gt; ?A3DomainTheory =
<div class=" highlight hl-gf"><pre><span></span>view A3SemanticsConstruction : http://mathhub.info/Teaching/lbs1920/Assignment3.gf?Assignment3 -&gt; ?A3DomainTheory =
// TODO fill in missing things ❙
john = john&#39;
......
......@@ -188,7 +188,7 @@
"metadata": {},
"outputs": [],
"source": [
"view A3SemanticsConstruction : http://mathhub.info/teaching/lbs1920/Assignment3.gf?Assignment3 -> ?A3DomainTheory =\n",
"view A3SemanticsConstruction : http://mathhub.info/Teaching/lbs1920/Assignment3.gf?Assignment3 -> ?A3DomainTheory =\n",
" // TODO fill in missing things ❙\n",
" \n",
" john = john' ❙\n",
......
namespace http://mathhub.info/teaching/lbs1920/assignment3 ❚
namespace http://mathhub.info/Teaching/lbs1920/assignment3 ❚
theory plnq : ur:?LF =
proposition : type ❘ # o ❙
......@@ -17,7 +17,7 @@ theory A3DomainTheory : ?plnq =
// TODO ❙
view A3SemanticsConstruction : http://mathhub.info/teaching/lbs1920/assignment3/Assignment3.gf?Assignment3 -> ?A3DomainTheory =
view A3SemanticsConstruction : http://mathhub.info/Teaching/lbs1920/assignment3/Assignment3.gf?Assignment3 -> ?A3DomainTheory =
// TODO ❙
john = john' ❙
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment