Add Polymorphic Sorts and Functions#3652

Merged

Drodt merged 34 commits intomainfrom

drodt/polymorphic

Mar 13, 2026

Commits on Aug 4, 2025

Start on polymorphic sorts and functions
Drodt
committed

Commits on Aug 13, 2025

Commits on Aug 14, 2025

Commits on Aug 18, 2025

Merge branch 'main' into drodt/polymorphic
Drodt
committed

Commits on Sep 24, 2025

Commits on Sep 25, 2025

Commits on Sep 26, 2025

Fix proof loading/storing when generics are instantiated in NoFindTaclets
Drodt
committed

Commits on Oct 30, 2025

Commits on Mar 9, 2026

Start on polymorphic sorts and functions

Drodt
authored and
wadoon
committed
Fix SortDepFn and add test

Drodt
authored and
wadoon
committed
Fix fns and preds parsing; add test

Drodt
authored and
wadoon
committed
Finish example; slight fixes

Drodt
authored and
wadoon
committed
Spotless

Drodt
authored and
wadoon
committed
Prepare datatype handling

Drodt
authored and
wadoon
committed
Fix taclets for datatypes w/ polymorphic params

Drodt
authored and
wadoon
committed
Slightly improve error messages

Drodt
authored and
wadoon
committed
Fix test classes

Drodt
authored and
wadoon
committed
Some documentation

Drodt
authored and
wadoon
committed
Fix proof loading/storing when generics are instantiated in NoFindTaclets

Drodt
authored and
wadoon
committed
Fix parsing of proof files

Drodt
authored and
wadoon
committed
Fix inst with sort depending fn

Drodt
authored and
wadoon
committed

Commits on Mar 10, 2026

Remove tokens file
Drodt
committed
Simplify
Drodt
committed

Commits on Mar 12, 2026