search

hferee / UIML

Uniform Interpolation for Modal Logics
Other
4 stars 1 forks source link

Strong induction is already part of StdLib #1

Closed DmxLarchey closed 4 months ago

DmxLarchey commented 4 months ago

https://github.com/hferee/UIML/blob/fffd11232f674759415c3337be9c7bdab7d35b00/theories/general/strong_inductionT.v#L5

Require Import Arith.

Check (well_founded_induction_type lt_wf).
hferee commented 4 months ago

Thank you @DmxLarchey . This folder is rather old legacy code ; there is probably a lot more to clean up there!