Code

Predicate support#656

Code

Merged

tobiasgrosser merged 19 commits intomainopencompl/lean-mlir:mainfrom predicate_supportopencompl/lean-mlir:predicate_supportCopy head branch name to clipboardSep 28, 2024

+509-74

Commits

Commits on Sep 25, 2024

• chore: update to nightly-2024-09-25

  tobiasgrosser

  committed
  0a7092b

• chore: predicate support in FSM

  tobiasgrosser

  committed
  e8354ea

• Add types

  tobiasgrosser

  committed
  77d89e6

• Format

  tobiasgrosser

  committed
  7e2a2ab

• Connect termEvalEq

  tobiasgrosser

  committed
  1c11c84

• Merge remote-tracking branch 'origin/main' into predicate_support

  tobiasgrosser

  committed
  d3b4310

• Update SSA/Experimental/Bits/Fast/FiniteStateMachine.lean

  Show description for 16342fd
  

  tobiasgrosser

  and

  alexkeizer

  authored
  16342fd

Commits on Sep 26, 2024

• chore: progress

  bollu

  committed
  74b9b9e

• WIP: start repeatBit implementation

  alexkeizer

  committed
  674e094

• Merge branch 'predicate_support' of github.com:opencompl/lean-mlir into predicate_support

  alexkeizer

  committed
  d4f6360

• repeatBit combinator

  alexkeizer

  committed
  cd16f5c

• chore: define and, or.

  bollu

  committed
  c3ecbf3

Commits on Sep 28, 2024

• remove sorry from corec

  

  Atticus Kuhn

  committed
  74d8de7

• simplify proof

  

  Atticus Kuhn

  committed
  40d1330

• simpify proof

  

  Atticus Kuhn

  committed
  a49220f

• chore: fix sorry, now allow project to build. We fail on guard_msgs due to sorry?

  bollu

  committed
  9d1d2b2

• chore: allow project to compile by updating guard messages with sorry

  bollu

  committed
  b5e09db

• chore: cleanup

  bollu

  committed
  92ff7c0

• chore: duplicate Defs, Lemmas into Fast

  bollu

  committed
  49405aa