lambdapi icon indicating copy to clipboard operation
lambdapi copied to clipboard
verified publisher icon Deducteam

Error in HRS output

Open fblanqui opened this issue 5 years ago • 1 comments

In a rule LHS, type annotations of abstractions are replaced by the same variable m_typ: https://github.com/Deducteam/lambdapi/blob/82dccc5074bd42574d8d21b9b39527052d2014cd/src/core/hrs.ml#L38

fblanqui avatar Jun 02 '20 11:06 fblanqui

This artificially creates non-linear rules.

fblanqui avatar Jun 02 '20 13:06 fblanqui

Fixed in #871

fblanqui avatar Aug 01 '23 10:08 fblanqui