mirror of
https://gitlab.kit.edu/uskyk/typicalc.git
synced 2024-11-08 10:20:41 +00:00
Exchange and add example term
This commit is contained in:
parent
bf31ae5096
commit
7310eec398
@ -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) {
|
||||
|
@ -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 | \
|
||||
|
Loading…
Reference in New Issue
Block a user