From 7310eec3981405c529052dacc3b0713cbdedf939 Mon Sep 17 00:00:00 2001
From: Moritz Dieing <63721811+moritzdieing@users.noreply.github.com>
Date: Sun, 18 Jul 2021 14:25:21 +0200
Subject: [PATCH] Exchange and add example term

---
 .../edu/kit/typicalc/view/main/ExampleDialog.java  |  2 +-
 src/main/resources/language/general.properties     | 14 ++++++++------
 2 files changed, 9 insertions(+), 7 deletions(-)

diff --git a/src/main/java/edu/kit/typicalc/view/main/ExampleDialog.java b/src/main/java/edu/kit/typicalc/view/main/ExampleDialog.java
index 8d5f97d..8f6d023 100644
--- a/src/main/java/edu/kit/typicalc/view/main/ExampleDialog.java
+++ b/src/main/java/edu/kit/typicalc/view/main/ExampleDialog.java
@@ -61,7 +61,7 @@ public class ExampleDialog extends Dialog implements LocaleChangeObserver {
         add(headingLayout, container);
         setId(EXAMPLE_DIALOG_ID);
         setWidth("392px");
-        setHeight("661px");
+        setHeight("670px");
     }
     
     private void setAssumptionExamples(String term) {
diff --git a/src/main/resources/language/general.properties b/src/main/resources/language/general.properties
index 713ee3e..02ea1f3 100644
--- a/src/main/resources/language/general.properties
+++ b/src/main/resources/language/general.properties
@@ -8,9 +8,10 @@ root.examplebutton=\uD83D\uDCC2
 root.exampleTerms=\
   λx.x,\
   λx.λy.y x,\
-  λx.λy.y (x x),\
+  (λx.x true) (y g),\
   let f = λx. g y y in f 3,\
   let k = λx.λy. x in k a (k b c),\
+  let f = (λx.y x) (y 5) in λg.f 3,\
   (λx.x x) (λx.x x),\
   (λx.λy.y (x y)) (λz. λa. z g a),\
   let f = λx. let g = λy. y in g x in f 3,\
@@ -18,12 +19,13 @@ root.exampleTerms=\
   
 root.λx.x=∅
 root.λx.λy.yx=∅
-root.λx.λy.y(xx)=∅
-root.letfλx.gyyinf3=∅;g: a->b->a;g: int->int->bool;g: int->int->bool, y: bool;g: int->int->bool, y: τ₁
-root.letkλx.λy.xinka(kbc)=∅;a: τ₁;a: ∀τ₁.τ₁->int, b: a;a: int, b: bool, c: char
+root.(λx.xtrue)(yg)=∅;y: int->boolean->τ₁, g: boolean;y: int->boolean->τ₁, g: τ₁;y: int->boolean->τ₁, g: ∀τ₁.τ₁
+root.letfλx.gyyinf3=∅;g: a->b->a;g: int->int->boolean;g: int->int->boolean, y: bool;g: int->int->boolean, y: τ₁
+root.letkλx.λy.xinka(kbc)=∅;a: τ₁;a: ∀τ₁.τ₁->int, b: a;a: int, b: boolean, c: char
+root.letf(λx.yx)(y5)inλg.f3=∅;y: int->(int->boolean);y: τ₁->(int->boolean);y: ∀τ₁.τ₁->(int->boolean)
 root.(λx.xx)(λx.xx)=∅
-root.(λx.λy.y(xy))(λz.λa.zga)=∅;g: bool;a: int, g: bool->int;g: ∀τ₂.τ₁->τ₂
-root.letfλx.letgλy.yingxinf3=∅;g: bool->int->bool
+root.(λx.λy.y(xy))(λz.λa.zga)=∅;g: boolean;a: int, g: boolean->int;g: ∀τ₂.τ₁->τ₂
+root.letfλx.letgλy.yingxinf3=∅;g: boolean->int->boolean
 root.letfλx.letgλy.55ingxinf3=∅
  
 root.termGrammar=\u2329Term\u232A ::= (\u2329Term\u232A) | \u2329App\u232A | \u2329Abs\u232A | \