From 3abd18ce48b5f39dd9749d7e3a359db82af40833 Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Mon, 29 Dec 2025 09:49:07 -0800
Subject: [PATCH] updates to playground help/comments

---
 playground/samples/Reasoning.newt | 37 +++++++++++++++----------------
 playground/src/help.md            |  2 +-
 2 files changed, 19 insertions(+), 20 deletions(-)

diff --git a/playground/samples/Reasoning.newt b/playground/samples/Reasoning.newt
index e74c50e..78140c4 100644
--- a/playground/samples/Reasoning.newt
+++ b/playground/samples/Reasoning.newt
@@ -1,48 +1,47 @@
 module Reasoning
 
-infix 4 _≡_
-data _≡_ : {A : U} → A → A → U where
-  Refl : ∀ A. {x : A} → x ≡ x
+-- From the "Lists" chapter of Programming Language Foundations in Agda
+-- https://plfa.github.io/Lists/
 
-sym : ∀ A. {x y : A} → x ≡ y → y ≡ x
+-- We define a few types and functions on lists and prove a couple of properties
+-- about them. This example demonstrates mixfix operators.
+
+infix 4 _≡_
+data _≡_ : ∀ A. A → A → U where
+  Refl : ∀ A. {0 x : A} → x ≡ x
+
+sym : ∀ A. {0 x y : A} → x ≡ y → y ≡ x
 sym Refl = Refl
 
-trans : ∀ A. {x y z : A} → x ≡ y → y ≡ z → x ≡ z
+trans : ∀ A. {0 x y z : A} → x ≡ y → y ≡ z → x ≡ z
 trans Refl eq = eq
 
-cong : ∀ A B. (f : A → B) {x y : A}
+cong : ∀ A B. (0 f : A → B) {0 x y : A}
   → x ≡ y
   → f x ≡ f y
 cong f Refl = Refl
 
-cong-app : ∀ A B. {f g : A → B}
+cong-app : ∀ A B. {0 f g : A → B}
   → f ≡ g
-  → (x : A) →  f x ≡ g x
+  → (0 x : A) →  f x ≡ g x
 cong-app Refl = λ y => Refl
 
 infixl 1 begin_
 infixr 2 _≡⟨⟩_ _≡⟨_⟩_
 infixl 3 _∎
 
-begin_ : ∀ A. {x y : A} → x ≡ y → x ≡ y
+begin_ : ∀ A. {0 x y : A} → x ≡ y → x ≡ y
 begin x≡y = x≡y
 
-_≡⟨⟩_  : ∀ A. (x : A) {y : A} → x ≡ y → x ≡ y
+_≡⟨⟩_  : ∀ A. (0 x : A) {0 y : A} → x ≡ y → x ≡ y
 x ≡⟨⟩ x≡y = x≡y
 
-_≡⟨_⟩_ : ∀ A. (x : A) {y z : A} → x ≡ y → y ≡ z → x ≡ z
+_≡⟨_⟩_ : ∀ A. (0 x : A) {0 y z : A} → x ≡ y → y ≡ z → x ≡ z
 x ≡⟨ x≡y ⟩ y≡z = trans x≡y y≡z
 
-_∎ : ∀ A. (x : A) → x ≡ x
+_∎ : ∀ A. (0 x : A) → x ≡ x
 x ∎ = Refl
 
-
--- From the "Lists" chapter of Programming Language Foundations in Agda
--- https://plfa.github.io/Lists/
-
--- We define a few types and functions on lists and prove a couple of properties
--- about them
-
 -- Natural numbers are zero (Z) or the successor (S) of a natural number
 -- We'll use these to represent the length of lists
 data Nat : U where
diff --git a/playground/src/help.md b/playground/src/help.md
index ec19ad4..68cb876 100644
--- a/playground/src/help.md
+++ b/playground/src/help.md
@@ -2,7 +2,7 @@
 
 Newt is a dependent typed programming language that compiles to javascript. This playground embeds the newt compiler and a codemirror based editor.
 
-The editor will typecheck the file with newt and render errors as the file is changed. The current file is saved to localStorage and will be restored if there is no data in the URL. Cmd-s or Ctrl-s will create a url embedding the file contents. There is a layout toggle for phone use.
+The editor will typecheck the file with newt and render errors as the file is changed. The current file is saved to localStorage and will be restored if there is no data in the URL. Cmd-s or Ctrl-s will create a url embedding the file contents.
 
 ## Tabs