max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: add mising (Active)Target.with* utilities

Browse source
This commit is contained in:
tydeu 2021-09-16 17:03:15 -04:00
parent bf4db86bdd
commit 8b83d80956
1 changed files with 12 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
Lake/Target.lean
View file

@ -28,6 +28,9 @@ def withInfo (info : i') (self : ActiveTarget i n t) : ActiveTarget i' n t :=
def withoutInfo (self : ActiveTarget i n t) : ActiveTarget PUnit n t :=
self.withInfo ()
def withTask (task : n' t') (self : ActiveTarget i n t) : ActiveTarget i n' t' :=
{self with task}
def opaque (task : n t) : ActiveTarget PUnit n t :=
⟨(), task⟩
@ -94,6 +97,15 @@ instance [Inhabited i] [Inhabited t] [Pure m] [Pure n] : Inhabited (Target i m n
namespace Target
def withInfo (info : i') (self : Target i m n t) : Target i' m n t :=
{self with info}
def withoutInfo (self : Target i m n t) : Target PUnit m n t :=
self.withInfo ()
def withTask (task : m' (n' t')) (self : Target i m n t) : Target i m' n' t' :=
{self with task}
def opaque (task : m (n t)) : Target PUnit m n t :=
mk () task