Skip to content

Commit

Permalink
Fully qualify Definition for now
Browse files Browse the repository at this point in the history
  • Loading branch information
sankalpgambhir committed Nov 4, 2024
1 parent 7c8aa45 commit a497bb6
Showing 1 changed file with 1 addition and 1 deletion.
Original file line number Diff line number Diff line change
Expand Up @@ -231,7 +231,7 @@ object Substitution:
end Apply

object Unfold extends ProofTactic:
def apply(using lib: Library, proof: lib.Proof)(definition: Definition)(premise: proof.Fact): proof.ProofTacticJudgement =
def apply(using lib: Library, proof: lib.Proof)(definition: lib.theory.Definition)(premise: proof.Fact): proof.ProofTacticJudgement =
???


Expand Down

0 comments on commit a497bb6

Please sign in to comment.