Skip to content

Commit

Permalink
Push again a fix or simp
Browse files Browse the repository at this point in the history
  • Loading branch information
ymherklotz committed Oct 24, 2024
1 parent b072bab commit 782c56b
Showing 1 changed file with 5 additions and 4 deletions.
9 changes: 5 additions & 4 deletions DataflowRewriter/Examples/BranchMerge.lean
Original file line number Diff line number Diff line change
Expand Up @@ -38,14 +38,14 @@ section BranchMerge
deq [mod="io"];

m [mod="m"];
bag [mod="bag"];
bags [mod="bag"];
joiner [mod="join"];
-- Producing the tagged values
m -> joiner [out="out", inp="inp0"];
-- Push into the bag
joiner -> bag [out = "out0", inp = "enq"];
joiner -> bags [out = "out0", inp = "enq"];
-- Connecting with the exporting interface
bag -> deq [out="deq"];
bags -> deq [out="deq"];
enq -> m [inp ="inp"];
enqT -> joiner [inp="inp1"];
]
Expand All @@ -61,7 +61,8 @@ example y : (fun S TagT T input output internals =>
outputs := [(⟨ .top, "out"⟩ , output)].toAssocList,
internals := internals })⟩) = y := by
dsimp only [test,drunfold,seval,Batteries.AssocList.toList,bagged,Function.uncurry,Module.mapIdent,List.toAssocList,List.foldl,Batteries.AssocList.find?,Option.pure_def,Option.bind_eq_bind,Option.bind_some,Module.renamePorts,Batteries.AssocList.mapKey,InternalPort.map,toString,Nat.repr,Nat.toDigits,Nat.toDigitsCore,Nat.digitChar,List.asString,Option.bind,Batteries.AssocList.mapVal,Batteries.AssocList.erase,Batteries.AssocList.eraseP,beq_self_eq_true,Option.getD,cond,beq_self_eq_true, beq_iff_eq, InternalPort.mk.injEq, String.reduceEq, and_false, imp_self,BEq.beq]
simp only [seval,InternalPort.mk.injEq, and_false, decide_False, decide_True]
simp only [seval,InternalPort.mk.injEq, and_false, decide_False, decide_True, and_true]

-- nearly there
sorry

Expand Down

0 comments on commit 782c56b

Please sign in to comment.