Record Types Example

Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.

Record Types Example

theory RecordTest : http://mathhub.info/MitM/Foundation?Logic =
    value : type ❙
    empty : value ❙
    X : value ❙
    O : value ❙
    state : type ❘ = {'
        Faa : value ,
        Fab : value ,
        Fac : value
    '} ❙
    s : state ❘ = ['
        Faa := empty ,
        Fab := X ,
        Fac := O
    '] ❙
❚