search

UniFormal / MMT

The MMT Language and System
https://uniformal.github.io/
Other
68 stars 22 forks source link

Push-out facts are not simplified #585

Open MaZiFAU opened 6 months ago

MaZiFAU commented 6 months ago

Using FrameIT-mmt Rest-API will not simplify returned facts, but returnd entire AST. Though the AST may be desired in some cases, iff MMT is able to resolve a term, the simplified version is preferred.

For reproduction: use e.g. http://mathhub.info/FrameIT/frameworld?OppositeLen theory/Scroll via e.g. the UFrameIT-Game.

I have attached request, expected and actual answers for an application of scroll "http://mathhub.info/FrameIT/frameworld?RiverScroll" river_request.json apply_river_expected.json apply_river_actual.json

The facts listed in "river_request.json" are the following (ordered), and are added using fact/add endpoint (see Rest-API). Any ?fact<#nr> are dynamic and Ids returned from the server after sending an add request. River_1st.json River_2nd.json River_3rd.json River_4th.json River_4.5th.json River_5th.json (angle of facts # 2,3,1 a.k.a w,x,y)

Jazzpirate commented 5 months ago

Translation: 173=w: LFX/Sigma?Symbols?Tuple(-24.32552,1.83532131,1.56619191) 174=x: LFX/Sigma?Symbols?Tuple(-24.32552,0.7562289,1.56619227) 175=y: LFX/Sigma?Symbols?Tuple(-24.32552,0.7562289,2.64528465) 176=B: LFX/Sigma?Symbols?Tuple(-24.32552,-0.00494384766,-5.32920074) 367=B: LFX/Sigma?Symbols?Tuple(0.0,-9.81,0.0) 368: lhs: geometry?Geometry/Common?angle_between(174,175,173), rhs:45, kind:veq