Konrad Slind comments

Repositories
Issues
Comments

Results 23 comments of


                                            Konrad Slind

Update Definition syntaxes to allow declaration of types of new constants

It also supports prim. rec defns. in the list: TotalDefn.multiDefine `(f2 0 = 3) /\ (f2 (SUC n) = 1 + f2 n) /\ (f3 0 = f2 0) /\...

Update Definition syntaxes to allow declaration of types of new constants

And it supports wfrec defns when the auto-prover manages to solve the termination problem: TotalDefn.multiDefine `(f5 n = if n = 0n then 1 else n * f5 (n-1)) /\...

Update Definition syntaxes to allow declaration of types of new constants

And there is elaborate clique-finding etc so the order of the declarations doesn't matter. See https://github.com/HOL-Theorem-Prover/HOL/blob/2eff78b608efb12cbea315f4813b4f4af70793a0/src/tfl/src/Defn.sml#L1825 for where that stuff is implemented. It might be too elaborate ... I thought...