search

Deducteam / lambdapi

Proof assistant based on the λΠ-calculus modulo rewriting
Other
265 stars 35 forks source link

lambdapi fails when inputing a metavariable #985

Open fblanqui opened 1 year ago

fblanqui commented 1 year ago 
symbol a:A;
symbol f : A → A → A;
symbol i:A → A;

symbol lem : A ≔
begin
apply f { print ?1 } { };
end;
// [/home/blanqui/src/lambdapi/tmp/zo.lp:8:16-18] Unknown object ?1.