wikifn-fstar

Extracted F* Playground

This page drives the earlier nine-function artifact, kept because it is the only place that shows three distinct compilation paths for the same composition: an interpreted IR, a generated direct function, and a hand-written reference. The engine does not have that split.

For the current work, with thousands of compositions, use the engine browser.

The page loads the generated JavaScript, but it does not run examples until a button is pressed.

Demos menu

Fixed Examples

Runs a small suite through the generated F* IR interpreter, generated direct F* functions, and hand-maintained F* reference functions.

Ready. Nothing has run yet.
What ran Input Result from extracted JS Source path

Raw JSON lines from the browser artifact:


      


      

        
Callable Selected Functions

        

          These are selected real Wikifunctions composition paths currently
          generated into F* and exposed through the browser artifact.
        

        

          
          
          
          
          
        

        

      


      

        
JSON IR

        

          This small expression format is useful for testing supported scalar
          primitives and selected calls without writing a full Wikifunctions
          object.
        

        

          
          
        

        

      


      

        
Supported Z7 Call

        

          This is the beginning of the real Wikifunctions object adapter:
          selected Z7 calls and selected value forms lower into the
          extracted F* evaluator. Unsupported objects fail at the boundary.