Purescala BNF (WIP) - epfl-lara/leon GitHub Wiki
| program | object id { definition * } |
| classdef | |
| definition | classdef |
| fundef | |
| classdef | abstract class id [ { fundef * } ]? |
| case class id ( args ) [ extends id ]? | |
| case object id [ extends id ]? | |
| fundef | def id ( decls ) : type = { [ require( expr ) ]? expr } [ ensuring( id => * expr ) ]? |